awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
n : ℕ
x : α
hxt : x ∉ t
⊢ Eq.{u_2 + 1} (α := β) ((S n ∩ t).indicator (⇑(f_approx n) : (a : α) → β) x) 0
have refine : x ∉ S n ∩ t
Tactic: refine Set.indicator_of_notMem ?_ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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)
⊢ FinStronglyMeasurable f μ
have h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
Tactic: have h_fs_t_compl : ∀ n, ∀ x, x ∉ t → fs n x = 0 := by
    intro n x hxt
    rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]
    refine Set.indicator_of_notMem ?_ _
    simp [hxt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β)
⊢ FinStronglyMeasurable f μ
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fs, ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ FinStronglyMeasurable f μ
have refine_2 : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: refine ⟨fs, ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: simp_rw [SimpleFunc.support_eq, ← Finset.mem_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have 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∞)
Tactic: refine fun n => measure_biUnion_lt_top {y ∈ (fs n).range | y ≠ 0}.finite_toSet fun y hy => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 β)
refine_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1₁ : y ≠ 0
Tactic: rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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_1 : 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 β)
this : (y : β) → Decidable (y = 0) := fun (y : β) ↦ Classical.propDecidable (y = 0)
⊢ y ≠ 0
have hy₁ : y ∈ (fs n).range ∧ y ≠ 0
Tactic: rw [Finset.mem_coe, Finset.mem_filter] at hy
Cleared hypotheses: hy, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine (measure_mono Set.inter_subset_left).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
have h_lt_top : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
have 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∞)
Tactic: rwa [Measure.restrict_apply' ht] at h_lt_top
Cleared hypotheses: h_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have refine_1₂ : ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)), y ≠ 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have refine_1₆ : ∀ (n : ℕ) (y : β) (hy : y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have pos : ∀ (hxt : x ∈ t), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: by_cases hxt : x ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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))
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have neg : ∀ (hxt : x ∉ t), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: by_cases hxt : x ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have neg : Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
Tactic: rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]