-- 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:
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 {x | ((fun n => f n x) '' u N) ×ˢ ((fun n => f n x) '' u N) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 1)}}

Tactic:
simp_rw [prod_image_image_eq, image_subset_iff, prod_subset_iff, 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)
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)}})

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
    (⋂ 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)}})

Tactic:
refine MeasurableSet.biInter Set.countable_univ fun K _ => ?_

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
    {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)}}

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 (⋃ 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)}})

Tactic:
refine MeasurableSet.iUnion fun N => ?_

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
N : ℕ
⊢ MeasurableSet {x | ((fun n => f n x) '' u N) ×ˢ ((fun n => f n x) '' u N) ⊆ {p | dist p.1 p.2 < 1 / (↑K + 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
⊢ MeasurableSet {x | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}

Tactic:
letI := upgradePolishSpace γ

Result:
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)}

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 | ∃ c, Tendsto (fun n => f n x) l (𝓝 c)}

Tactic:
simp_rw [← cauchy_map_iff_exists_tendsto]

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 | Cauchy (map (fun n => f n x) l)}

Proof state:
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)}

Tactic:
simp

Result:
no goals