-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem measurableSet_exists_tendsto [TopologicalSpace γ] [PolishSpace γ] [MeasurableSpace γ]
    [hγ : OpensMeasurableSpace γ] [Countable ι] {l : Filter ι}
    [l.IsCountablyGenerated] {f : ι → β → γ} (hf : ∀ i, Measurable (f i)) :
    MeasurableSet { x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c) }

Proof state:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}

Tactic:
rcases l.eq_or_neBot with rfl | hl

Result:
case inl
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inst✝ : ⊥.IsCountablyGenerated
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) ⊥ (𝓝 c)}

case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}

Proof state:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n =>
      ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)
⊢ MeasurableSet {x | (map (fun n => f n x) l).NeBot ∧ map (fun n => f n x) l ×ˢ map (fun n => f n x) l ≤ uniformity γ}

Tactic:
simp_rw [and_iff_right (hl.map _),
  Filter.HasBasis.le_basis_iff (this _).toHasBasis Metric.uniformity_basis_dist_inv_nat_succ,
  Set.setOf_forall]

Result:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n =>
      ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)
⊢ MeasurableSet
    (⋂ i,
      ⋂ (_ : True),
        {x |
          ∃ i_2, True ∧ ((fun n => f n x) '' u i_2) ×ˢ ((fun n => f n x) '' u i_2) ⊆ {p | dist p.1 p.2 < 1 / (↑i + 1)}})

Proof state:
case inr
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedPolishSpace γ := upgradePolishSpace γ
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}

Tactic:
rcases l.exists_antitone_basis with ⟨u, hu⟩

Result:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}

Proof state:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | Cauchy (map (fun n => f n x) l)}

Tactic:
change MeasurableSet { x | _ ∧ _ }

Result:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | (map (fun n => f n x) l).NeBot ∧ map (fun n => f n x) l ×ˢ map (fun n => f n x) l ≤ uniformity γ}

Proof state:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n =>
      ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i => True
N : ℕ
⊢ MeasurableSet
    (⋂ i ∈ u N, ⋂ i_1 ∈ u N, {x | (i, i_1) ∈ (fun p => (f p.1 x, f p.2 x)) ⁻¹' {p | dist p.1 p.2 < 1 / (↑K + 1)}})

Tactic:
exact
  MeasurableSet.biInter (to_countable (u N)) fun i _ =>
    MeasurableSet.biInter (to_countable (u N)) fun j _ =>
      measurableSet_lt (Measurable.dist (hf i) (hf j)) measurable_const

Result:
no goals

Proof state:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n =>
      ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i => True
⊢ MeasurableSet
    {x | ∃ i, True ∧ ((fun n => f n x) '' u i) ×ˢ ((fun n => f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}

Tactic:
simp_rw [Set.setOf_exists, true_and]

Result:
case inr.intro
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁵ : MeasurableSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : PolishSpace γ
inst✝² : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst✝¹ : Countable ι
l : Filter ι
inst✝ : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this✝ : UpgradedPolishSpace γ := upgradePolishSpace γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (map (fun x_1 => f x_1 x) l ×ˢ map (fun x_1 => f x_1 x) l).HasAntitoneBasis fun n =>
      ((fun x_1 => f x_1 x) '' u n) ×ˢ ((fun x_1 => f x_1 x) '' u n)
K : ℕ
x✝ : K ∈ fun i => True
⊢ MeasurableSet (⋃ i, {x | ((fun n => f n x) '' u i) ×ˢ ((fun n => f n x) '' u i) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}})