awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
n : ℕ
y : β
hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (spanningSets (μ.restrict t) n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h_lt_top := measure_spanningSets_lt_top (μ.restrict t) n
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
n : ℕ
y : β
hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)
h_lt_top : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (spanningSets (μ.restrict t) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀ (h_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets (μ.restrict t) n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [Measure.restrict_apply' ht] at h_lt_top

Premises used: MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
refine_1 :
  ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1₁ :
  ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
refine_1₂ refine_1₃ : ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)), y ≠ 0
refine_1₄ refine_1₅ :
  ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
refine_1₆ :
  ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1₇ :
  ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β))
    (h_lt_top :
      LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) (spanningSets (μ.restrict t) n) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
classical
    refine fun n => measure_biUnion_lt_top {y ∈ (fs n).range | y ≠ 0}.finite_toSet fun y hy => ?_
    rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]
    swap
    · letI : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable _
      rw [Finset.mem_coe, Finset.mem_filter] at hy
      exact hy.2
    refine (measure_mono Set.inter_subset_left).trans_lt ?_
    have h_lt_top := measure_spanningSets_lt_top (μ.restrict t) n
    rwa [Measure.restrict_apply' ht] at h_lt_top

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, Finset.mem_filter, MeasureTheory.Measure.restrict_apply', LE.le.trans_lt, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
pos : ∀ (hxt : x ∈ t), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
neg : ∀ (hxt : x ∉ t), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
by_cases hxt : x ∈ t
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∉ t
neg : Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]

Premises used: funext
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∉ t
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∉ t
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
⊢ Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
have h : Tendsto (fun n => (f_approx n) x) atTop (𝓝 (f x)) := hf_meas.tendsto_approx x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
rsuffices : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → x ∈ S m), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
rsuffices₁ : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t

Tactic:
rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t

Tactic:
⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩

Premises used: Set.mem_inter, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t

Tactic:
exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
rsuffices : ∀ (n : ℕ) (hn : x ∈ S n), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
rsuffices₁ : ∃ (n : ℕ), x ∈ S n
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m

Tactic:
rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : x ∈ S n
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m

Tactic:
⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩

Premises used: MeasureTheory.monotone_spanningSets, MeasureTheory.Measure.restrict, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : x ∈ S n
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m

Tactic:
exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
rw : Membership.mem (γ := Set α) univ x
⊢ ∃ (n : ℕ), x ∈ S n

Tactic:
rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]

Premises used: Set.mem_iUnion, MeasureTheory.Measure.restrict, MeasureTheory.iUnion_spanningSets
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Membership.mem (γ := Set α) univ x

Tactic:
trivial
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
obtain :
  ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t),
    ∃ (n : ℕ),
      ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
⊢ ∃ (n : ℕ),
    ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)

Tactic:
obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
⊢ ∃ (n : ℕ),
    ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)

Tactic:
⟨n, fun m hnm => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
refine :
  ∀ (m_1 : ℕ) (hnm : n ≤ m_1), Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
⊢ ∃ (n : ℕ),
    ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)

Tactic:
refine ⟨n, fun m hnm => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m_1 : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
m : ℕ
hnm : n ≤ m
simp_rw :
  Eq.{u_2 + 1} (α := β) (((f_approx m).restrict (S m ∩ t) : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
simp_rw₁ :
  Eq.{u_2 + 1} (α := β) ((S m ∩ t).indicator (⇑(f_approx m) : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((fs m : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)

Tactic:
simp_rw [fs, SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
        Set.indicator_of_mem (hn m hnm)]

Premises used: Set.indicator_of_mem, MeasureTheory.SimpleFunc.restrict_apply, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
pos :
  ∀ (n₁ : ℕ)
    (hn₁ :
      ∀ (m_1 : ℕ),
        n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)),
    Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
obtain ⟨n₁, hn₁⟩ : ∃ n, ∀ m, n ≤ m → fs m x = f_approx m x := by
      obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial
      refine ⟨n, fun m hnm => ?_⟩
      simp_rw [fs, SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
        Set.indicator_of_mem (hn m hnm)]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
pos :
  ∀ (h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)) (n₁ : ℕ)
    (hn₁ :
      ∀ (m_1 : ℕ),
        n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)),
    ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
rw [tendsto_atTop'] at h ⊢

Premises used: Filter.tendsto_atTop'