awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
⊢ y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ y ∈ sᶜ
have pos : Eq.{u_6 + 1} (α := E) ((g_seq_s n : (a : α) → E) y : E) (0 : E) ∧ y ∈ sᶜ ↔ y ∈ sᶜ
Tactic: rw [hx, Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
this : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have rw : MeasurableSet.{u_5} (α := α) ∅
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ MeasurableSet (preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ)
have neg : preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
Tactic: suffices g_seq_s n ⁻¹' {x} ∩ sᶜ = ∅ by
            rw [this]
            exact MeasurableSet.empty
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ = ∅
have neg : ∀ (y : α), y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ Membership.mem (γ := Set α) ∅ y
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α
⊢ y ∈ preimage (β := E) (⇑(g_seq_s n) : (a : α) → E) {x} ∩ sᶜ ↔ Membership.mem (γ := Set α) ∅ y
have neg : (g_seq_s n : (a : α) → E) y = x → y ∈ s
Tactic: simp only [mem_inter_iff, mem_preimage, mem_singleton_iff, mem_compl_iff,
            mem_empty_iff_false, iff_false, not_and, not_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
have neg : ∀ (hys : y ∉ s), ¬(g_seq_s n : (a : α) → E) y = x
Tactic: refine Function.mtr fun hys => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ¬(g_seq_s n : (a : α) → E) y = x
have neg : ¬0 = x
Tactic: rw [hg_seq_zero y hys n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 α),
    (∀ (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
have 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
Tactic: obtain ⟨s, hs, hs_univ⟩ :=
    @exists_spanning_measurableSet_le _ m _ hf.nnnorm.measurable (μ.trim hm) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
have refine : ∀ (n : ℕ) (x : α) (hx : x ∈ s n), ‖f x‖ ≤ (↑n : ℝ)
Tactic: refine ⟨s, fun n ↦ ⟨(hs n).1, (le_trim hm).trans_lt (hs n).2.1, fun x hx ↦ ?_⟩, hs_univ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : ℝ)
have hx_nnnorm : ‖f x‖₊ ≤ (↑n : ℝ≥0)
Tactic: have hx_nnnorm : ‖f x‖₊ ≤ n := (hs n).2.2 x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
⊢ ‖f x‖ ≤ (↑n : ℝ)
have rw : (↑‖f x‖₊ : ℝ) ≤ (↑n : ℝ)
Tactic: rw [← coe_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : Zero β
inst_1 : TopologicalSpace β
inst_2 : T2Space β
hf : FinStronglyMeasurable f μ
⊢ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
have 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)
Tactic: rcases hf with ⟨fs, hT_lt_top, h_approx⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : α) → β)
⊢ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
have hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
Tactic: have hT_meas : ∀ n, MeasurableSet (T n) := fun n => SimpleFunc.measurableSet_support (fs n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have refine_1 : ∀ x ∈ tᶜ, f x = 0
Tactic: refine ⟨t, MeasurableSet.iUnion hT_meas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ∃ (t : Set α), MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
have refine_2 : SigmaFinite (μ.restrict t)
Tactic: refine ⟨t, MeasurableSet.iUnion hT_meas, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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ᶜ
⊢ Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
have hxt₁ : ∀ (x_1 : ℕ), x ∉ T x_1
Tactic: rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt
Cleared hypotheses: hxt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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
⊢ ∀ x ∈ tᶜ, f x = 0
have h_fs_zero : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
have refine_1 : ∀ (x : α) (hxt : x ∈ tᶜ), Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 0)
Tactic: refine fun x hxt => tendsto_nhds_unique (h_approx x) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 0)
have refine_1 : Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
Tactic: rw [funext fun n => h_fs_zero n x hxt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ SigmaFinite (μ.restrict t)
have refine_2 : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ tᶜ ∪ T n) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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_2 :
  ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ tᶜ ∪ T n) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite (μ.restrict t)
have refine_2₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ tᶜ ∪ T n) i) univ
Tactic: refine ⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ tᶜ ∪ T n) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (T n ∩ ⋃ (b : ℕ), T b) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply' (MeasurableSet.iUnion hT_meas), Set.union_inter_distrib_right,
        Set.compl_inter_self t, Set.empty_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ tᶜ ∪ T n) i) univ
have refine_2 : tᶜ ∪ ⋃ (i : ℕ), T i = univ
Tactic: rw [← Set.union_iUnion tᶜ T]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : MulZeroClass β
inst_2 : ContinuousMul β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f * g) μ
have n : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n * hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine
    ⟨fun n => hf.approx n * hg.approx n, ?_, fun x =>
      (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
⊢ FinStronglyMeasurable (-f) μ
have refine : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ -hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨fun n ↦ -hf.approx n, fun n ↦ ?_, fun x ↦ (hf.tendsto_approx x).neg⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ -hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have suffices : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: suffices μ (Function.support fun x ↦ -(hf.approx n) x) < ∞ by convert! this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
inst_1 : SubtractionMonoid β
inst_2 : ContinuousNeg β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) fun (x : α) ↦ -(hf.approx n : (a : α) → β) x) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑(hf.approx n) : (a : α) → β)) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [Function.support_fun_neg (hf.approx n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
⊢ FinStronglyMeasurable (c • f) μ
have refine : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ c • hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨fun n => c • hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).const_smul c⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : Zero β
inst_3 : SMulZeroClass 𝕜 β
inst_4 : ContinuousSMul 𝕜 β
hf : FinStronglyMeasurable f μ
c : 𝕜
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ c • hf.approx n) n) : (a : α) → β)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (support (HSMul.hSMul (β := (a : α) → β) c (⇑(hf.approx n) : (a : α) → β))) : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [SimpleFunc.coe_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst : TopologicalSpace β
inst_1 : Zero β
inst_2 : SemilatticeSup β
inst_3 : ContinuousSup β
hf : FinStronglyMeasurable f μ
hg : FinStronglyMeasurable g μ
⊢ FinStronglyMeasurable (f ⊔ g) μ
have n : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (support.{u_1, u_2} (M := β) (⇑((fun (n : ℕ) ↦ hf.approx n ⊔ hg.approx n) n) : (a : α) → β)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine
    ⟨fun n => hf.approx n ⊔ hg.approx n, fun n => ?_, fun x =>
      (hf.tendsto_approx x).sup_nhds (hg.tendsto_approx x)⟩