awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
x : α
h : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
h₅ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → ¬ContinuousWithinAt g t x
h₆ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₇ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₈ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₉ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₁₀ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₁₁ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₁₂ : x ∈ t → ContinuousWithinAt g t x → x ∉ t → False
h₁₃ : x ∈ t → ContinuousWithinAt g t x → ¬ContinuousWithinAt g t x → False
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
have : g '' t = g '' (t \ t') ∪ g '' t' := by
    rw [← image_union]
    congr!
    ext
    simp only [sdiff_sep_self, not_not, mem_union, mem_setOf_eq, t']
    tauto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
rw : MeasurableSet (g '' (t \ t') ∪ g '' t')
⊢ MeasurableSet (g '' t)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
apply : MeasurableSet (g '' (t \ t'))
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')

Tactic:
apply MeasurableSet.union _ (ht'.image g).measurableSet

Premises used: Set.Countable.measurableSet, Set.Countable.image, MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
apply : ContinuousOn g (t \ t')
⊢ MeasurableSet (g '' (t \ t'))

Tactic:
apply MeasurableSet.image_of_monotoneOn_of_continuousOn (ht.diff ht'.measurableSet)
    (hg.mono diff_subset)

Premises used: MeasurableSet.diff, Set.diff_subset, MeasurableSet.image_of_monotoneOn_of_continuousOn, Set.Countable.measurableSet, MonotoneOn.mono
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
⊢ x ∈ t ∧ ContinuousWithinAt g t x

Tactic:
simp only [sdiff_sep_self, not_not, mem_setOf_eq, t'] at hx

Premises used: Classical.not_not, Set.mem_setOf_eq, Set.sdiff_sep_self
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t ∧ ContinuousWithinAt g t x
⊢ ContinuousWithinAt g (t \ t') x

Tactic:
hx.2.mono diff_subset

Premises used: Set.diff_subset, And.right, ContinuousWithinAt.mono
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t ∧ ContinuousWithinAt g t x
⊢ ContinuousWithinAt g (t \ t') x

Tactic:
exact hx.2.mono diff_subset

Premises used: Set.diff_subset, And.right, ContinuousWithinAt.mono
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : AntitoneOn g t
⊢ MeasurableSet (g '' t)

Tactic:
(ht.image_of_monotoneOn hg.dual_right :)

Premises used: AntitoneOn.dual_right, OrderDual, MeasurableSet.image_of_monotoneOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
inst_4 : TopologicalSpace γ
inst_5 : SecondCountableTopology γ
inst_6 : PseudoMetrizableSpace γ
inst_7 : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
simp_rw : MeasurableSet.{u_5} (α := β) {x : β | Tendsto (β := ℝ) (fun (b : ι) ↦ dist (f b x) (g x)) l (𝓝 0)}
⊢ MeasurableSet.{u_5} (α := β) {x : β | Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))}

Tactic:
simp_rw [tendsto_iff_dist_tendsto_zero (f := fun n ↦ f n _)]

Premises used: tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
inst_4 : TopologicalSpace γ
inst_5 : SecondCountableTopology γ
inst_6 : PseudoMetrizableSpace γ
inst_7 : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet.{u_5} (α := β) {x : β | Tendsto (β := ℝ) (fun (b : ι) ↦ dist (f b x) (g x)) l (𝓝 0)}

Tactic:
measurableSet_tendsto (𝓝 0) (fun n ↦ (hf n).dist hg)

Premises used: nhds, Measurable.dist, OfNat.ofNat, measurableSet_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
inst_4 : TopologicalSpace γ
inst_5 : SecondCountableTopology γ
inst_6 : PseudoMetrizableSpace γ
inst_7 : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet.{u_5} (α := β) {x : β | Tendsto (β := ℝ) (fun (b : ι) ↦ dist (f b x) (g x)) l (𝓝 0)}

Tactic:
exact measurableSet_tendsto (𝓝 0) (fun n ↦ (hf n).dist hg)

Premises used: nhds, Measurable.dist, OfNat.ofNat, measurableSet_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥],
    MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 c)}
inr : ∀ (hl : l.NeBot), MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}

Tactic:
rcases l.eq_or_neBot with rfl | hl

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inst_6 : IsCountablyGenerated.{u_2} (α := ι) ⊥
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 c)}

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
inr :
  ∀ (u : ℕ → Set ι) (hu : l.HasAntitoneBasis u),
    MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}

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

Premises used: Filter.exists_antitone_basis
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
inr : MeasurableSet.{u_5} (α := β) {x : β | Cauchy.{u_3} (α := γ) (map (fun (n : ι) ↦ f n x) l)}
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}

Tactic:
simp_rw [← cauchy_map_iff_exists_tendsto]

Premises used: cauchy_map_iff_exists_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)

Tactic:
have : ∀ x, (map (f · x) l ×ˢ map (f · x) l).HasAntitoneBasis fun n =>
      ((f · x) '' u n) ×ˢ ((f · x) '' u n) := fun x => (hu.map _).prod (hu.map _)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
inr :
  MeasurableSet.{u_5} (α := β)
    (⋂ (i : ℕ),
      ⋂ (_ : True),
        {x : β |
          ∃ (i_2 : ℕ),
            True ∧
              SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i_2) ((fun (n : ι) ↦ f n x) '' u i_2) ⊆
                {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1}})
⊢ MeasurableSet.{u_5} (α := β)
    {x : β |
      NeBot.{u_3} (α := γ) (map (fun (n : ι) ↦ f n x) l) ∧
        SProd.sprod (α := Filter γ) (β := Filter γ) (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]

Premises used: Filter.HasAntitoneBasis.toHasBasis, Metric.uniformity_basis_dist_inv_nat_succ, Filter.HasBasis.le_basis_iff, Filter.NeBot.map, and_iff_right, Set.setOf_forall
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
⊢ MeasurableSet.{u_5} (α := β)
    (⋂ (i : ℕ),
      ⋂ (_ : True),
        {x : β |
          ∃ (i_2 : ℕ),
            True ∧
              SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i_2) ((fun (n : ι) ↦ f n x) '' u i_2) ⊆
                {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1}})

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

Premises used: Set.Mem, Set.countable_univ, MeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
inr :
  ∀ (K : ℕ),
    Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K →
      MeasurableSet.{u_5} (α := β)
        {x : β |
          ∃ (i : ℕ),
            True ∧
              SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
                {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}
⊢ MeasurableSet.{u_5} (α := β)
    (⋂ (i : ℕ),
      ⋂ (_ : True),
        {x : β |
          ∃ (i_2 : ℕ),
            True ∧
              SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i_2) ((fun (n : ι) ↦ f n x) '' u i_2) ⊆
                {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1}})

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

Premises used: Set.countable_univ, MeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
K : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K
inr :
  MeasurableSet.{u_5} (α := β)
    (⋃ (i : ℕ),
      {x : β |
        SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
          {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}})
⊢ MeasurableSet.{u_5} (α := β)
    {x : β |
      ∃ (i : ℕ),
        True ∧
          SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
            {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}

Tactic:
simp_rw [Set.setOf_exists, true_and]

Premises used: Set.setOf_exists, true_and
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
K : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K
⊢ MeasurableSet.{u_5} (α := β)
    (⋃ (i : ℕ),
      {x : β |
        SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
          {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}})

Tactic:
MeasurableSet.iUnion fun N => ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
K : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K
inr :
  ∀ (N : ℕ),
    MeasurableSet.{u_5} (α := β)
      {x : β |
        SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u N) ((fun (n : ι) ↦ f n x) '' u N) ⊆
          {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}
⊢ MeasurableSet.{u_5} (α := β)
    (⋃ (i : ℕ),
      {x : β |
        SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i) ((fun (n : ι) ↦ f n x) '' u i) ⊆
          {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}})

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

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
K : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) K
N : ℕ
inr :
  MeasurableSet.{u_5} (α := β)
    (⋂ i ∈ u N,
      ⋂ i_1 ∈ u N,
        {x : β |
          Membership.mem (γ := Set (ι × ι))
            (preimage.{u_2, u_3} (β := γ × γ) (fun (p : ι × ι) ↦ (f p.1 x, f p.2 x))
              {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1})
            (i, i_1)})
⊢ MeasurableSet.{u_5} (α := β)
    {x : β |
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u N) ((fun (n : ι) ↦ f n x) '' u N) ⊆
        {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑K : ℝ) 1}}

Tactic:
simp_rw [prod_image_image_eq, image_subset_iff, prod_subset_iff, Set.setOf_forall]

Premises used: Set.prod_subset_iff, Set.prod_image_image_eq, Set.image_subset_iff, Set.setOf_forall