awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
neg : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)

Tactic:
suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = ∅ by
            rw [this]
            exact MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
neg : ∀ (y : α), y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ Membership.mem (γ := Set α) ∅ y
⊢ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅

Tactic:
ext1 y
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
y : α
neg : (g_seq_s n : (a : α) → E) y = x → y ∈ s
⊢ y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ Membership.mem (γ := Set α) ∅ y

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_singleton_iff, mem_compl_iff,
            mem_empty_iff_false, iff_false, not_and, not_notMem]

Premises used: iff_false, Set.mem_inter_iff, Set.not_notMem, Set.mem_singleton_iff, Set.mem_empty_iff_false, not_and, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
y : α
⊢ (g_seq_s n : (a : α) → E) y = x → y ∈ s

Tactic:
Function.mtr fun hys => ?_

Premises used: Function.mtr
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
y : α
neg : ∀ (hys : y ∉ s), ¬(g_seq_s n : (a : α) → E) y = x
⊢ (g_seq_s n : (a : α) → E) y = x → y ∈ s

Tactic:
refine Function.mtr fun hys => ?_

Premises used: Function.mtr
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : y ∉ s
neg : ¬0 = x
⊢ ¬(g_seq_s n : (a : α) → E) y = x

Tactic:
rw [hg_seq_zero y hys n]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : y ∉ s
⊢ ¬0 = x

Tactic:
Ne.symm hx

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
n : ℕ
x : E
hx : ¬x = 0
y : α
hys : y ∉ s
⊢ ¬0 = x

Tactic:
exact Ne.symm hx

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
g_seq_s₂ : ℕ → α →ₛ E :=
  fun (n : ℕ) ↦ { toFun := (⇑(g_seq_s n) : (a : α) → E), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
⟨g_seq_s₂, hg_seq_tendsto⟩

Premises used: Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
E : Type u_6
m m₂ : MeasurableSpace α
inst : TopologicalSpace E
inst_1 : Zero E
s : Set α
f : α → E
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
hs_m₂ : MeasurableSet s
g_seq_s : ℕ → α →ₛ E
hg_seq_tendsto : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (g_seq_s n : (a : α) → E) x) atTop (𝓝 (f x))
hg_seq_zero : ∀ x ∉ s, ∀ (n : ℕ), Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) x : E) (0 : E)
g_seq_s₂ : ℕ → α →ₛ E :=
  fun (n : ℕ) ↦ { toFun := (⇑(g_seq_s n) : (a : α) → E), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
exact ⟨g_seq_s₂, hg_seq_tendsto⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst_1 : SigmaFinite (μ.trim hm)
obtain :
  ∀ (s : ℕ → Set α)
    (hs :
      ∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ (↑n : ℝ≥0))
    (hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ),
    ∃ (s : ℕ → Set α),
      (∀ (n : ℕ),
          MeasurableSet (s n) ∧
            LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖ ≤ (↑n : ℝ)) ∧
        Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖ ≤ (↑n : ℝ)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ

Tactic:
obtain ⟨s, hs, hs_univ⟩ :=
    @exists_spanning_measurableSet_le _ m _ hf.nnnorm.measurable (μ.trim hm) _

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.Measure.trim, exists_spanning_measurableSet_le, MeasureTheory.StronglyMeasurable.nnnorm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst_1 : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs :
  ∀ (n : ℕ),
    MeasurableSet (s n) ∧
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ (↑n : ℝ≥0)
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖ ≤ (↑n : ℝ)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ

Tactic:
⟨s, fun n ↦ ⟨(hs n).1, (le_trim hm).trans_lt (hs n).2.1, fun x hx ↦ ?_⟩, hs_univ⟩

Premises used: MeasureTheory.le_trim, And.right, And.left, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst_1 : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs :
  ∀ (n : ℕ),
    MeasurableSet (s n) ∧
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ (↑n : ℝ≥0)
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
refine : ∀ (n : ℕ) (x : α) (hx : x ∈ s n), ‖f x‖ ≤ (↑n : ℝ)
⊢ ∃ (s : ℕ → Set α),
    (∀ (n : ℕ),
        MeasurableSet (s n) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖ ≤ (↑n : ℝ)) ∧
      Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ

Tactic:
refine ⟨s, fun n ↦ ⟨(hs n).1, (le_trim hm).trans_lt (hs n).2.1, fun x hx ↦ ?_⟩, hs_univ⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst_1 : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs :
  ∀ (n : ℕ),
    MeasurableSet (s n) ∧
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ (↑n : ℝ≥0)
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
n : ℕ
x : α
hx : x ∈ s n
⊢ ‖f x‖₊ ≤ (↑n : ℝ≥0)

Tactic:
have hx_nnnorm : ‖f x‖₊ ≤ n := (hs n).2.2 x hx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst_1 : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs :
  ∀ (n : ℕ),
    MeasurableSet (s n) ∧
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ (↑n : ℝ≥0)
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
n : ℕ
x : α
hx : x ∈ s n
hx_nnnorm : ‖f x‖₊ ≤ (↑n : ℝ≥0)
rw : (↑‖f x‖₊ : ℝ) ≤ (↑n : ℝ)
⊢ ‖f x‖ ≤ (↑n : ℝ)

Tactic:
rw [← coe_nnnorm]

Premises used: coe_nnnorm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst_1 : SigmaFinite (μ.trim hm)
s : ℕ → Set α
hs :
  ∀ (n : ℕ),
    MeasurableSet (s n) ∧
      LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∀ x ∈ s n, ‖f x‖₊ ≤ (↑n : ℝ≥0)
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
n : ℕ
x : α
hx : x ∈ s n
hx_nnnorm : ‖f x‖₊ ≤ (↑n : ℝ≥0)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ‖f x‖₊ ≤ (↑n : ℝ≥0)
⊢ (↑‖f x‖₊ : ℝ) ≤ (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_5
β : Type u_6
m : MeasurableSpace α
μ : Measure α
inst : Zero β
inst_1 : TopologicalSpace β
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_5, u_6} (M := β) (⇑(0 n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [Pi.zero_apply, SimpleFunc.coe_zero, support_zero, measure_empty,
      zero_lt_top, forall_const]

Premises used: ENNReal.zero_lt_top, MeasureTheory.SimpleFunc.coe_zero, Pi.zero_apply, MeasureTheory.measure_empty, Function.support_zero, forall_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
hf : FinStronglyMeasurable f μ
⊢ ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
hf.choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
hf : FinStronglyMeasurable f μ
⊢ ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
hf.choose_spec.2

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
hf : FinStronglyMeasurable f μ
⊢ StronglyMeasurable f

Tactic:
⟨hf.approx, hf.tendsto_approx⟩

Premises used: MeasureTheory.FinStronglyMeasurable.tendsto_approx, MeasureTheory.FinStronglyMeasurable.approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
hf : FinStronglyMeasurable f μ
rcases :
  ∀ (fs : ℕ → α →ₛ β)
    (hT_lt_top :
      ∀ (n : ℕ),
        LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞)
          (∞ : ℝ≥0∞))
    (h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))),
    ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
rcases hf with ⟨fs, hT_lt_top, h_approx⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
⊢ ∀ (n : ℕ), MeasurableSet (T n)

Tactic:
have hT_meas : ∀ n, MeasurableSet (T n) := fun n => SimpleFunc.measurableSet_support (fs n)
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
⊢ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
⟨t, MeasurableSet.iUnion hT_meas, ?_, ?_⟩

Premises used: And.intro, Exists.intro, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
refine_1 : ∀ x ∈ tᶜ, f x = 0
refine_2 : SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
refine ⟨t, MeasurableSet.iUnion hT_meas, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
n : ℕ
x : α
hxt : x ∈ tᶜ
⊢ ∀ (x_1 : ℕ), x ∉ T x_1

Tactic:
rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt

Premises used: Set.mem_iUnion, not_exists, Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
n : ℕ
x : α
hxt : ∀ (x_1 : ℕ), x ∉ T x_1
⊢ Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)

Tactic:
simpa [T] using hxt n
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
⊢ ∀ (n : ℕ), ∀ x ∈ tᶜ, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)

Tactic:
have h_fs_zero : ∀ n, ∀ x ∈ tᶜ, fs n x = 0 := by
      intro n x hxt
      rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt
      simpa [T] using hxt n
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
⊢ ∀ x ∈ tᶜ, f x = 0

Tactic:
fun x hxt => tendsto_nhds_unique (h_approx x) ?_

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
refine_1 : ∀ (x : α) (hxt : x ∈ tᶜ), Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 0)
⊢ ∀ x ∈ tᶜ, f x = 0

Tactic:
refine fun x hxt => tendsto_nhds_unique (h_approx x) ?_

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ tᶜ
refine_1 : Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 0)

Tactic:
rw [funext fun n => h_fs_zero n x hxt]

Premises used: funext
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
h_fs_zero : ∀ (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
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_approx : ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
T : (n : ℕ) → Set α := fun (n : ℕ) ↦ support.{u_1, u_2} (M := β) (⇑(fs n) : (a : α) → β)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ (n : ℕ), T n
h_fs_zero : ∀ (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