-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
/-- The set of points for which a sequence of measurable functions converges to a given value
is measurable. -/
@[measurability]
lemma measurableSet_tendsto {_ : MeasurableSpace β} [MeasurableSpace γ]
    [Countable δ] {l : Filter δ} [l.IsCountablyGenerated]
    (l' : Filter γ) [l'.IsCountablyGenerated] [hl' : l'.IsMeasurablyGenerated]
    {f : δ → β → γ} (hf : ∀ i, Measurable (f i)) :
    MeasurableSet { x | Tendsto (fun n ↦ f n x) l l' }

Proof state:
case intro.intro.intro
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun i => id (v i)
⊢ MeasurableSet (⋂ i, ⋃ i_1, ⋂ i_2 ∈ u i_1, {x | f i_2 x ∈ id (v i)})

Tactic:
exact .iInter fun n ↦ .iUnion fun _ ↦ .biInter (to_countable _) fun i _ ↦
  (v_meas n).2.preimage (hf i)

Result:
no goals

Proof state:
case intro
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l l'}

Tactic:
rcases (Filter.hasBasis_self.mpr hl'.exists_measurable_subset).exists_antitone_subbasis with
  ⟨v, v_meas, hv⟩

Result:
case intro.intro.intro
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun i => id (v i)
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l l'}

Proof state:
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l l'}

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

Result:
case intro
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l l'}

Proof state:
case intro.intro.intro
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun i => id (v i)
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l l'}

Tactic:
simp only [hu.tendsto_iff hv.toHasBasis, true_imp_iff, true_and, setOf_forall, setOf_exists]

Result:
case intro.intro.intro
β : Type u_2
γ : Type u_3
δ : Type u_4
x✝ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
inst✝² : Countable δ
l : Filter δ
inst✝¹ : l.IsCountablyGenerated
l' : Filter γ
inst✝ : l'.IsCountablyGenerated
hl' : l'.IsMeasurablyGenerated
f : δ → β → γ
hf : ∀ (i : δ), Measurable (f i)
u : ℕ → Set δ
hu : l.HasAntitoneBasis u
v : ℕ → Set γ
v_meas : ∀ (i : ℕ), v i ∈ l' ∧ MeasurableSet (v i)
hv : l'.HasAntitoneBasis fun i => id (v i)
⊢ MeasurableSet (⋂ i, ⋃ i_1, ⋂ i_2 ∈ u i_1, {x | f i_2 x ∈ id (v i)})