awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ Tendsto.{u_3, u_1} (β := (x : α) → ℝ≥0) (fun (i : ι) (x : α) ↦ infNndist (f i x) s) u
    (𝓝 fun (x : α) ↦ infNndist (g x) s)
have rw : ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))),
  let this := pseudoMetrizableSpacePseudoMetric β;
  ∀ (s : Set β) (h1s : IsClosed s) (h2s : s.Nonempty) (h3s : s ≠ Set.univ) (x : α),
    Tendsto (fun (i : ι) ↦ infNndist (f i x) s) u (𝓝 (infNndist (g x) s))
Tactic: rw [tendsto_pi_nhds] at lim ⊢
Cleared hypotheses: lim, this, s, h1s, h2s, h3s
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ MeasurableSet (g ⁻¹' s)
have this₁ : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
Tactic: have : Measurable fun x => infNndist (g x) s := by
    suffices Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s) from
      NNReal.measurable_of_tendsto' u (fun i => (hf i).infNndist) this
    rw [tendsto_pi_nhds] at lim ⊢
    intro x
    exact ((continuous_infNndist_pt s).tendsto (g x)).comp (lim x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
⊢ g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}
have h : ∀ (x : α), x ∈ g ⁻¹' s ↔ Membership.mem (γ := Set α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
⊢ MeasurableSet (g ⁻¹' s)
have h4s : g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}
Tactic: have h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0} := by
    ext x
    simp [← h1s.mem_iff_infDist_zero h2s, ← NNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
h4s : g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}
⊢ MeasurableSet (g ⁻¹' s)
have hf₁ : MeasurableSet.{u_1} (α := α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0})
Tactic: rw [h4s]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ AEMeasurable g μ
have rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
Tactic: rcases u.exists_seq_tendsto with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ AEMeasurable g μ
have h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
Tactic: have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x fun (n : ℕ) ↦ f (v n) x) x} x}
    a
Tactic: filter_upwards [h_tendsto] with x hx using hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x fun (n : ℕ) ↦ f (v n) x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
have h₁ : ∀ (a : α), Tendsto (fun (n : ι) ↦ f n a) u (𝓝 (g a)) → p a fun (n : ℕ) ↦ f (v n) a
Tactic: filter_upwards [h_tendsto] with x hx using hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
⊢ AEMeasurable g μ
have hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
Tactic: have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ AEMeasurable g μ
have refine_1 : ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
Tactic: refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
refine_1 : ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
⊢ AEMeasurable g μ
have refine_2 : g =ᶠ[ae μ] aeSeqLim
Tactic: refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
⊢ Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
have refine_1 : Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) sorry x else Nonempty.some sorry) atTop
  (𝓝 (if x ∈ aeSeqSet h'f p then g x else sorry.some))
Tactic: simp_rw [aeSeqLim, aeSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
⊢ Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
have pos : ∀ (hx : x ∈ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) sorry x) atTop (𝓝 (g x))
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
pos : ∀ (hx : x ∈ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))
⊢ Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
have neg : ∀ (hx : x ∉ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ Nonempty.some sorry) atTop (𝓝 sorry.some)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))
have pos : Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))
Tactic: simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ AEMeasurable g μ
have rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
Tactic: classical
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
  set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
  set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
  refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
  · simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds
  · exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
⊢ AEMeasurable g μ
have rcases₁ : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ), AEMeasurable g μ
Tactic: classical
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
  set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
  set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
  refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
  · simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds
  · exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
rcases₁ rcases₂ : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ), AEMeasurable g μ
⊢ AEMeasurable g μ
have rcases₃ : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ),
  let p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x));
  ∀ (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x), AEMeasurable g μ
Tactic: classical
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
  set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
  set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
  refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
  · simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds
  · exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
rcases₁ rcases₂ : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ), AEMeasurable g μ
rcases₃ rcases₄ :
  ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ),
    let p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x));
    ∀ (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x), AEMeasurable g μ
⊢ AEMeasurable g μ
have refine_1 : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ),
  let p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x));
  ∀ (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x),
    let aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else sorry.some;
    ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
Tactic: classical
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
  set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
  set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
  refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
  · simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds
  · exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm