awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ ≃ ι
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 : α
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) : ℕ))) ⋯ n :
          (a : α) → β)
        x)
    atTop (nhds (f (hs.index (s := s) x) 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))

Tactic:
simp only [simpleFunc_piecewise, SimpleFunc.coe_mk, piecewise_apply]

Premises used: IndexedPartition.simpleFunc_piecewise, MeasureTheory.SimpleFunc.coe_mk, IndexedPartition.piecewise_apply
-- 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 : ℕ ≃ ι
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 : α
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
⊢ ∀ᶠ (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)

Premises used: Equiv.bijective, And.right, IndexedPartition.index
-- 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 : ℕ ≃ ι
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

Tactic:
eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩

Premises used: Iff.mpr, HAdd.hAdd, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- 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 : ℕ ≃ ι
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
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
⊢ ∀ᶠ (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:
refine eventually_atTop.mpr ⟨y + 1, fun b hb => ?_⟩

Premises used: Iff.mpr, HAdd.hAdd, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- 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 : ℕ ≃ ι
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
⊢ y < b + 1

Tactic:
lia
-- 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 : ℕ ≃ ι
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
⊢ y = (↑(⟨y, ⋯⟩ : Fin (b + 1)) : ℕ)

Tactic:
have : y = (⟨y, by lia⟩ : Fin (b + 1)).1 := rfl
-- 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 : ℕ ≃ ι
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)) : ℕ)
rw : Membership.mem (γ := Set α) (⋃ i ∈ g b ⁻¹' {(⟨y, ⋯⟩ : Fin (b + 1))}, s i) x
⊢ (e : (a : ℕ) → ι) (↑((G b).index (s := fun (k : Fin (b + 1)) ↦ ⋃ i ∈ g b ⁻¹' {k}, s i) x) : ℕ) = hs.index (s := s) x

Tactic:
rw [← hy, EmbeddingLike.apply_eq_iff_eq, this, ← Fin.ext_iff, ← (G b).mem_iff_index_eq]

Premises used: Fin.ext_iff, IndexedPartition.mem_iff_index_eq, EmbeddingLike.apply_eq_iff_eq
-- 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 : ℕ ≃ ι
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)) : ℕ)
⊢ y < b

Tactic:
lia
-- 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 : ℕ ≃ ι
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)) : ℕ)
⊢ ∃ m < b, hs.index (s := s) x = (e : (a : ℕ) → ι) m

Tactic:
have : ∃ m < b, hs.index x = e m := ⟨y, ⟨by lia, hy.symm⟩⟩
-- 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 : ℕ ≃ ι
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_1 : y = (↑(⟨y, ⋯⟩ : Fin (b + 1)) : ℕ)
this : ∃ m < b, hs.index (s := s) x = (e : (a : ℕ) → ι) m
⊢ Membership.mem (γ := Set α) (⋃ i ∈ g b ⁻¹' {(⟨y, ⋯⟩ : Fin (b + 1))}, s i) x

Tactic:
simpa [g, hs.mem_iff_index_eq, this] using e.injective (hy.trans this.choose_spec.2).symm

Premises used: Exists.choose_spec, IndexedPartition.mem_iff_index_eq, And.right, Equiv.injective, Eq.symm, Eq.trans
-- 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 : ℕ ≃ ι
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

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
-- 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 : ℕ ≃ ι
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
rw rw₁ :
  Eq.{u_3 + 1} (α := β) ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) ⋯ n : (a : α) → β) x : β)
    ((StronglyMeasurable.approx (f := f (hs.index (s := s) x)) ⋯ n : (a : α) → β) 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 :
      β)

Tactic:
rw [hn]
-- 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 : ℕ ≃ ι
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
h₁ h₂ :
  ∀ (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 :
        β)
⊢ ∀ᶠ (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 :
        β)

Tactic:
filter_upwards [this] with n hn using by rw [hn]
-- 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 : ℕ ≃ ι
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 :
        β)

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]
-- 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 : ℕ ≃ ι
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_1 :
  ∀ᶠ (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 (x_1 : ℕ) ↦ (StronglyMeasurable.approx (f := f (hs.index (s := s) x)) ⋯ x_1 : (a : α) → β) x) atTop
    (nhds (f (hs.index (s := s) x) x))

Tactic:
simp [StronglyMeasurable.tendsto_approx]

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx
-- 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 : ℕ ≃ ι
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_1 :
  ∀ᶠ (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))

Tactic:
exact (Filter.tendsto_congr' this).mp (by simp [StronglyMeasurable.tendsto_approx])

Premises used: Iff.mp, Filter.tendsto_congr'
-- Module: Mathlib.MeasureTheory.Function.Piecewise
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
choose :
  ∀ (p : (i : ι) → α → β) (hp : ∀ (i : ι), StronglyMeasurable (p i)) (hq : ∀ (i : ι), f i =ᶠ[ae μ] p i),
    AEStronglyMeasurable (hs.piecewise (s := s) f) μ
⊢ AEStronglyMeasurable (hs.piecewise (s := s) f) μ

Tactic:
choose p hp hq using hf
-- Module: Mathlib.MeasureTheory.Function.Piecewise
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
⊢ AEStronglyMeasurable (hs.piecewise (s := s) f) μ

Tactic:
⟨hs.piecewise p, hs.stronglyMeasurable_piecewise hm hp, ?_⟩

Premises used: IndexedPartition.piecewise, And.intro, Exists.intro, IndexedPartition.stronglyMeasurable_piecewise, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.Piecewise
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
refine : hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
⊢ AEStronglyMeasurable (hs.piecewise (s := s) f) μ

Tactic:
refine ⟨hs.piecewise p, hs.stronglyMeasurable_piecewise hm hp, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Piecewise
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
x : α
hx : ∀ (i : ι), f i x = p i x
⊢ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x

Tactic:
hx (hs.index x)

Premises used: IndexedPartition.piecewise, IndexedPartition.index
-- Module: Mathlib.MeasureTheory.Function.Piecewise
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
p : (i : ι) → α → β
hp : ∀ (i : ι), StronglyMeasurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), f i a = p i a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x) x}
            x}
      a
h₁ h₂ : ∀ (x : α) (hx : ∀ (i : ι), f i x = p i x), hs.piecewise (s := s) f x = hs.piecewise (s := s) p x
⊢ hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p

Tactic:
filter_upwards [ae_all_iff.2 hq] with x hx using hx (hs.index x)

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f g : α →ₛ β
H : Eq (α := (a : α) → β) (⇑f : (a : α) → β) (⇑g : (a : α) → β)
⊢ f = g

Tactic:
DFunLike.ext' H

Premises used: DFunLike.ext'
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f g : α →ₛ β
H : ∀ (a : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((g : (a : α) → β) a : β)
⊢ f = g

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
f : α →ₛ β
⊢ Set.Finite.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β))

Tactic:
f.finite_range'

Premises used: MeasureTheory.SimpleFunc.finite_range'