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 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c

Tactic:
have : ∀ n, ∃ c, ∀ x, fs n x = c := fun n => SimpleFunc.simpleFunc_bot (fs n)
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
⊢ ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n

Tactic:
have h_cs_eq : ∀ n, ⇑(fs n) = fun _ => cs n := fun n => funext (this n).choose_spec
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h : ∀ (x : α) (n : ℕ), ((fs n : (a : α) → β) x : β)
| ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
enter [x, 1, n]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
x : α
n : ℕ
h : (fun (x : α) ↦ cs n) x
| ((fs n : (a : α) → β) x : β)

Tactic:
rw [h_cs_eq]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h : ∀ (x : α) (n : ℕ), (fun (x : α) ↦ cs n) x
| ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
enter [x, 1, n]; rw [h_cs_eq]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
⊢ ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))

Tactic:
conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h_fs_tendsto₁ : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
⊢ ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n

Tactic:
conv at h_fs_tendsto => enter [x, 1, n]; rw [h_cs_eq]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
⊢ Tendsto cs atTop (𝓝 (f hα.some))

Tactic:
have h_tendsto : Tendsto cs atTop (𝓝 (f hα.some)) := h_fs_tendsto hα.some
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
inr : ∀ (x : α), f x = f hα.some
⊢ f = fun (x : α) ↦ f hα.some

Tactic:
ext1 x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
x : α
⊢ f x = f hα.some

Tactic:
tendsto_nhds_unique (h_fs_tendsto x) h_tendsto

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
this : ∀ (n : ℕ), ∃ (c : β), ∀ (x : α), (fs n : (a : α) → β) x = c
cs : (n : ℕ) → β := fun (n : ℕ) ↦ ⋯.choose (p := fun (c : β) ↦ ∀ (x : α), (fs n : (a : α) → β) x = c)
h_fs_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fun (x : α) ↦ cs n) x) atTop (𝓝 (f x))
h_cs_eq : ∀ (n : ℕ), Eq (α := (a : α) → β) (⇑(fs n) : (a : α) → β) fun (x : α) ↦ cs n
h_tendsto : Tendsto cs atTop (𝓝 (f hα.some))
x : α
⊢ f x = f hα.some

Tactic:
exact tendsto_nhds_unique (h_fs_tendsto x) h_tendsto

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf_eq : ∃ (c : β), f = fun (x : α) ↦ c
inr : ∀ (c : β), StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c
⊢ StronglyMeasurable f

Tactic:
obtain ⟨c, rfl⟩ := hf_eq

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
c : β
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c

Tactic:
stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
c : β
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c

Tactic:
exact stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const
-- 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μ : SigmaFinite (μ.restrict t)
⊢ SigmaFinite (μ.restrict t)

Tactic:
haveI : SigmaFinite (μ.restrict t) := htμ
-- 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)
⊢ ∀ (n : ℕ), MeasurableSet (S n)

Tactic:
have hS_meas : ∀ n, MeasurableSet (S n) := measurableSet_spanningSets (μ.restrict 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)
n : ℕ
x : α
hxt : x ∉ t
rw : Eq.{u_2 + 1} (α := β) ((S n ∩ t).indicator (⇑(f_approx n) : (a : α) → β) x) 0
⊢ Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)

Tactic:
rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]

Premises used: 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)
n : ℕ
x : α
hxt : x ∉ t
⊢ Eq.{u_2 + 1} (α := β) ((S n ∩ t).indicator (⇑(f_approx n) : (a : α) → β) x) 0

Tactic:
Set.indicator_of_notMem ?_ _

Premises used: Set.indicator_of_notMem
-- 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)
n : ℕ
x : α
hxt : x ∉ t
refine : x ∉ S n ∩ t
⊢ Eq.{u_2 + 1} (α := β) ((S n ∩ t).indicator (⇑(f_approx n) : (a : α) → β) x) 0

Tactic:
refine Set.indicator_of_notMem ?_ _

Premises used: Set.indicator_of_notMem
-- 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)
n : ℕ
x : α
hxt : x ∉ t
⊢ x ∉ S n ∩ t

Tactic:
simp [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)
⊢ ∀ (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]
-- 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 : β)
⊢ FinStronglyMeasurable f μ

Tactic:
⟨fs, ?_, fun x => ?_⟩

Premises used: And.intro, Exists.intro, MeasureTheory.FinStronglyMeasurable
-- 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 : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ FinStronglyMeasurable f μ

Tactic:
refine ⟨fs, ?_, fun 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 : β)
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp_rw [SimpleFunc.support_eq, ← Finset.mem_coe]

Premises used: MeasureTheory.SimpleFunc.support_eq, 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 : β)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
fun n => measure_biUnion_lt_top {y ∈ (fs n).range | y ≠ 0}.finite_toSet fun y hy => ?_

Premises used: MeasureTheory.measure_biUnion_lt_top, Ne, Finset.finite_toSet, MeasureTheory.SimpleFunc.range, OfNat.ofNat, Finset.filter
-- 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∞)
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋃ y ∈ (↑({y ∈ (fs n).range | y ≠ 0}) : Set β), 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 => ?_

Premises used: MeasureTheory.measure_biUnion_lt_top, Ne, Finset.finite_toSet, MeasureTheory.SimpleFunc.range, OfNat.ofNat, Finset.filter
-- 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 β)
refine_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
refine_1₁ : y ≠ 0
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β) (⇑(fs n) : (a : α) → β) {y}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]

Premises used: MeasureTheory.SimpleFunc.restrict_preimage_singleton, 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_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 ∈ (fs n).range ∧ y ≠ 0

Tactic:
rw [Finset.mem_coe, Finset.mem_filter] at hy

Premises used: Finset.mem_filter, 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_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 ∈ (fs n).range ∧ y ≠ 0
this : (y : β) → Decidable (y = 0) := fun (y : β) ↦ Classical.propDecidable (y = 0)
⊢ y ≠ 0

Tactic:
hy.2

Premises used: And.right
-- 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_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 ∈ (fs n).range ∧ y ≠ 0
this : (y : β) → Decidable (y = 0) := fun (y : β) ↦ Classical.propDecidable (y = 0)
⊢ y ≠ 0

Tactic:
exact hy.2

Premises used: And.right
-- 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∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
(measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- 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 β)
refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n ∩ t ∩ preimage (β := β) (⇑(f_approx n) : (a : α) → β) {y}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
refine (measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt