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
μ : 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 μ
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 ⋯.some;
      ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
⊢ AEMeasurable g μ
have refine_2 : ∀ (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;
    g =ᶠ[ae μ] aeSeqLim
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
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
⊢ AEMeasurable g μ
have obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), AEMeasurable g μ
Tactic: obtain ⟨u, -, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ AEMeasurable g μ
have choose : ∀ (f : (n : ℕ) → α → β) (Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n),
  AEMeasurable g μ
Tactic: choose f Hf using fun n : ℕ => hf (u n) (u_pos n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
have this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
Tactic: have : ∀ᵐ x ∂μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 fun n => (Hf n).2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
have h : ∀ (a : α), (∀ (n : ℕ), dist (f n a) (g a) ≤ u n) → Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (g a))
Tactic: filter_upwards [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
have h : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist (f b x) (g x)) atTop (𝓝 0)
Tactic: rw [tendsto_iff_dist_tendsto_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
⊢ AEMeasurable g μ
have this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Tactic: have : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) := by
    have : ∀ᵐ x ∂μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 fun n => (Hf n).2
    filter_upwards [this]
    intro x hx
    rw [tendsto_iff_dist_tendsto_zero]
    exact squeeze_zero (fun n => dist_nonneg) hx u_lim
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inhabit : ∀ (inhabited_h : Inhabited ι),
  ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: inhabit ι
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inl : ∀ [IsCountablyGenerated.{u_3} (α := ι) ⊥]
  (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)),
  ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))
Tactic: rcases eq_or_neBot L with (rfl | hL)
Cleared hypotheses: L, inst_7, h_ae_tendsto
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
inl :
  ∀ [IsCountablyGenerated.{u_3} (α := ι) ⊥]
    (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inr : ∀ (hL : L.NeBot), ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: rcases eq_or_neBot L with (rfl | hL)
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have h : ∀ (x : α) (hx : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: filter_upwards [h_ae_tendsto] with x hx
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have hf_lim : AEMeasurable f_lim μ
Tactic: have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inr : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
Tactic: refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
f_lim : α → β :=
  fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else ⋯.some
h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
hf_lim : AEMeasurable f_lim μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
have h : ∀ (x : α) (hx : Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))) (h_eq : f_lim x = AEMeasurable.mk f_lim hf_lim x),
  Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
Tactic: filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inhabit : ∀ (inhabited_h : Inhabited ι),
  ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: classical
  inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabit :
  ∀ (inhabited_h : Inhabited ι),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inl : ∀ (inhabited_h : Inhabited ι) [IsCountablyGenerated.{u_3} (α := ι) ⊥]
  (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)),
  ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))
Tactic: classical
  inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using hx
Cleared hypotheses: L, inst_7, h_ae_tendsto
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabit :
  ∀ (inhabited_h : Inhabited ι),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
inl :
  ∀ (inhabited_h : Inhabited ι) [IsCountablyGenerated.{u_3} (α := ι) ⊥]
    (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inr : ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
  ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: classical
  inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabit :
  ∀ (inhabited_h : Inhabited ι),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
inl :
  ∀ (inhabited_h : Inhabited ι) [IsCountablyGenerated.{u_3} (α := ι) ⊥]
    (h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 l)),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 (f_lim x))
inr inr₁ inr₂ :
  ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
have inr₃ : ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
  let f_lim : α → β := fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else sorry.some;
  ∀ (h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
Tactic: classical
  inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using hx