awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : β)
x : α
hxt : x ∈ t
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: have h : Tendsto (fun n => (f_approx n) x) atTop (𝓝 (f x)) := hf_meas.tendsto_approx x
-- 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
have rsuffices : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → x ∈ S m), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
Tactic: rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
-- 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
rsuffices : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → x ∈ S m), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
have rsuffices₁ : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
Tactic: rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
-- 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
have rsuffices : ∀ (n : ℕ) (hn : x ∈ S n), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
Tactic: rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S 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 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
rsuffices : ∀ (n : ℕ) (hn : x ∈ S n), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → x ∈ S m
have rsuffices₁ : ∃ (n : ℕ), x ∈ S n
Tactic: rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S 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 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∃ (n : ℕ), x ∈ S n
have rw : Membership.mem (γ := Set α) univ x
Tactic: rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∃ (n : ℕ),
    ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
have obtain : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t),
  ∃ (n : ℕ),
    ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
Tactic: obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial
-- 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
⊢ ∃ (n : ℕ),
    ∀ (m_1 : ℕ), n ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
have refine : ∀ (m_1 : ℕ) (hnm : n ≤ m_1), Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
Tactic: refine ⟨n, fun m hnm => ?_⟩
-- 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_1 : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
m : ℕ
hnm : n ≤ m
simp_rw :
  Eq.{u_2 + 1} (α := β) (((f_approx m).restrict (S m ∩ t) : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
⊢ Eq.{u_2 + 1} (α := β) ((fs m : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
have simp_rw₁ : Eq.{u_2 + 1} (α := β) ((S m ∩ t).indicator (⇑(f_approx m) : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
Tactic: simp_rw [fs, SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
        Set.indicator_of_mem (hn m hnm)]
-- 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have pos : ∀ (n₁ : ℕ)
  (hn₁ :
    ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)),
  Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: obtain ⟨n₁, hn₁⟩ : ∃ n, ∀ m, n ≤ m → fs m x = f_approx m x := by
      obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial
      refine ⟨n, fun m hnm => ?_⟩
      simp_rw [fs, SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
        Set.indicator_of_mem (hn m hnm)]
-- 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
h : Tendsto (fun (n : ℕ) ↦ (f_approx n : (a : α) → β) x) atTop (𝓝 (f x))
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
⊢ Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))
have pos : ∀ (h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)) (n₁ : ℕ)
  (hn₁ :
    ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)),
  ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)
Tactic: rw [tendsto_atTop'] at h ⊢
Cleared hypotheses: h, n₁, hn₁
-- 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
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
⊢ ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)
have pos : ∀ (n₂ : ℕ) (hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)),
  ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)
Tactic: obtain ⟨n₂, hn₂⟩ := h s hs
-- 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
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
⊢ ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)
have pos : ∀ (m_1 : ℕ) (hm : m_1 ≥ max n₁ n₂), Membership.mem (α := β) s ((fs m_1 : (a : α) → β) x : β)
Tactic: refine ⟨max n₁ n₂, fun m hm => ?_⟩
-- 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_1 : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → Eq.{u_2 + 1} (α := β) ((fs m : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
m : ℕ
hm : m ≥ max n₁ n₂
⊢ Membership.mem (α := β) s ((fs m : (a : α) → β) x : β)
have pos : Membership.mem (α := β) s ((f_approx m : (a : α) → β) x : β)
Tactic: rw [hn₁ m ((le_max_left _ _).trans hm.le)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : One β
inst_1 : TopologicalSpace β
inst_2 : MetrizableSpace β
hf : StronglyMeasurable f
⊢ MeasurableSet (mulSupport f)
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (β := β × γ) fun (x : α) ↦ (f x, g x)
have refine : ∀ (x : α),
  Tendsto (β := β × γ) (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
    (𝓝 ((fun (x : α) ↦ (f x, g x)) x))
Tactic: refine ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (β := β × γ) (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
    (𝓝 ((fun (x : α) ↦ (f x, g x)) x))
have rw : Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
  (𝓝 (f x) ×ˢ 𝓝 (g x))
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f / g)
have refine : ∀ (x : α),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
Tactic: refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
have this : MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}
Tactic: have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
this : MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
have pos : ∀ (h : g x = 0),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
Tactic: by_cases h : g x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
this : MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}
pos :
  ∀ (h : g x = 0),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
      atTop (𝓝 ((f / g) x))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
have neg : ∀ (h : ¬g x = 0),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
Tactic: by_cases h : g x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
this : MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}
h : g x = 0
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
have pos : ∀ (this : MeasurableSet.{u_1} (α := α) {x : α | ¬g x = 0}) (h : g x = 0),
  Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
Tactic: simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_setOf_eq,
      not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
this : MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}
h : ¬g x = 0
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))
have neg : ∀ (this : MeasurableSet.{u_1} (α := α) {x : α | ¬g x = 0}) (h : ¬g x = 0),
  Tendsto
    (fun (n : ℕ) ↦ HDiv.hDiv (α := β) (β := β) ((hf.approx n : (a : α) → β) x : β) ((hg.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x / g x))
Tactic: simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
      Pi.div_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddCancelMonoid E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g + f)
have rcases : ∀ (φ : ℕ → α →ₛ E) (hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))),
  Measurable (g + f)
Tactic: rcases hf with ⟨φ, hφ⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddCancelMonoid E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))
⊢ Measurable (g + f)
have this : Tendsto (fun (n : ℕ) (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)) atTop (𝓝 (g + f))
Tactic: have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) :=
    tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))