awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
⊢ ∀ (p : A),
    ∃ (q : Set β),
      f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q ∧
        Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) q ∧ MeasurableSet q

Tactic:
have : ∀ p : A, ∃ q : Set β,
      f '' (p.1.1 : Set γ) ⊆ q ∧ Disjoint (f '' (p.1.2 : Set γ)) q ∧ MeasurableSet q := by
    intro p
    apply
      AnalyticSet.measurablySeparable ((hb.isOpen p.1.1.2).analyticSet_image f_cont)
        ((hb.isOpen p.1.2.2).analyticSet_image f_cont)
    exact Disjoint.image p.2 f_inj.injOn (subset_univ _) (subset_univ _)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
this :
  ∀ (p : A),
    ∃ (q : Set β),
      f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q ∧
        Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) q ∧ MeasurableSet q
choose :
  ∀ (q : (p : A) → Set β) (hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p)
    (hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p))
    (q_meas : ∀ (p : A), MeasurableSet (q p)), MeasurableSet (range f)
⊢ MeasurableSet (range f)

Tactic:
choose q hq1 hq2 q_meas using this
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
⊢ ∃ (u : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
obtain :
  ∀ (u : ℕ → ℝ) (u_anti : StrictAnti u) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)),
    MeasurableSet (range f)
⊢ MeasurableSet (range f)

Tactic:
obtain ⟨u, u_anti, u_pos, u_lim⟩ :
      ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b_1 : Set (Set γ)
b_count : b_1.Countable
b_nonempty : ∅ ∉ b_1
hb : IsTopologicalBasis b_1
this_2 : Encodable (↑b_1 : Type u_3)
A : Type (max 0 u_3) := { p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b_1 : Type u_3) → Set β :=
  fun (s : (↑b_1 : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b_1 : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b_1 : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
b : (↑b_1 : Type u_3)
⊢ MeasurableSet (E b)

Tactic:
isClosed_closure.measurableSet.inter ?_

Premises used: IsClosed.measurableSet, isClosed_closure, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b_1 : Set (Set γ)
b_count : b_1.Countable
b_nonempty : ∅ ∉ b_1
hb : IsTopologicalBasis b_1
this_2 : Encodable (↑b_1 : Type u_3)
A : Type (max 0 u_3) := { p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b_1 : Type u_3) → Set β :=
  fun (s : (↑b_1 : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b_1 : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b_1 : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
b : (↑b_1 : Type u_3)
refine :
  MeasurableSet.{u_4} (α := β)
    (⋂ (t : (↑b_1 : Type u_3)),
      ⋂ (ht : Disjoint (↑b : Set γ) (↑t : Set γ)),
        q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (b, t) ht) \
          q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (t, b) ⋯))
⊢ MeasurableSet (E b)

Tactic:
refine isClosed_closure.measurableSet.inter ?_

Premises used: IsClosed.measurableSet, isClosed_closure, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b_1 : Set (Set γ)
b_count : b_1.Countable
b_nonempty : ∅ ∉ b_1
hb : IsTopologicalBasis b_1
this_2 : Encodable (↑b_1 : Type u_3)
A : Type (max 0 u_3) := { p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b_1 : Type u_3) → Set β :=
  fun (s : (↑b_1 : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b_1 : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b_1 : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
b : (↑b_1 : Type u_3)
⊢ MeasurableSet.{u_4} (α := β)
    (⋂ (t : (↑b_1 : Type u_3)),
      ⋂ (ht : Disjoint (↑b : Set γ) (↑t : Set γ)),
        q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (b, t) ht) \
          q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (t, b) ⋯))

Tactic:
MeasurableSet.iInter fun s => ?_

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b_1 : Set (Set γ)
b_count : b_1.Countable
b_nonempty : ∅ ∉ b_1
hb : IsTopologicalBasis b_1
this_2 : Encodable (↑b_1 : Type u_3)
A : Type (max 0 u_3) := { p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b_1 : Type u_3) → Set β :=
  fun (s : (↑b_1 : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b_1 : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b_1 : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
b : (↑b_1 : Type u_3)
refine :
  ∀ (s : (↑b_1 : Type u_3)),
    MeasurableSet.{u_4} (α := β)
      (⋂ (ht : Disjoint (↑b : Set γ) (↑s : Set γ)),
        q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (b, s) ht) \
          q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (s, b) ⋯))
⊢ MeasurableSet.{u_4} (α := β)
    (⋂ (t : (↑b_1 : Type u_3)),
      ⋂ (ht : Disjoint (↑b : Set γ) (↑t : Set γ)),
        q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (b, t) ht) \
          q
            (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (t, b) ⋯))

Tactic:
refine MeasurableSet.iInter fun s => ?_

Premises used: MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b_1 : Set (Set γ)
b_count : b_1.Countable
b_nonempty : ∅ ∉ b_1
hb : IsTopologicalBasis b_1
this_2 : Encodable (↑b_1 : Type u_3)
A : Type (max 0 u_3) := { p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b_1 : Type u_3) → Set β :=
  fun (s : (↑b_1 : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b_1 : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b_1 : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
b s : (↑b_1 : Type u_3)
⊢ MeasurableSet.{u_4} (α := β)
    (⋂ (ht : Disjoint (↑b : Set γ) (↑s : Set γ)),
      q
          (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
            (b, s) ht) \
        q
          (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
            (s, b) ⋯))

Tactic:
MeasurableSet.iInter fun hs => (q_meas _).diff (q_meas _)

Premises used: MeasurableSet.diff, Prod.mk, Subtype.mk, Disjoint.symm, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b_1 : Set (Set γ)
b_count : b_1.Countable
b_nonempty : ∅ ∉ b_1
hb : IsTopologicalBasis b_1
this_2 : Encodable (↑b_1 : Type u_3)
A : Type (max 0 u_3) := { p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b_1 : Type u_3) → Set β :=
  fun (s : (↑b_1 : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b_1 : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦
                Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ)) (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b_1 : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
b s : (↑b_1 : Type u_3)
⊢ MeasurableSet.{u_4} (α := β)
    (⋂ (ht : Disjoint (↑b : Set γ) (↑s : Set γ)),
      q
          (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
            (b, s) ht) \
        q
          (Subtype.mk (p := fun (p : (↑b_1 : Type u_3) × (↑b_1 : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
            (s, b) ⋯))

Tactic:
exact MeasurableSet.iInter fun hs => (q_meas _).diff (q_meas _)

Premises used: MeasurableSet.diff, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
⊢ ∀ (s : (↑b : Type u_3)), MeasurableSet (E s)

Tactic:
have E_meas : ∀ s : b, MeasurableSet (E s) := by
      intro b
      refine isClosed_closure.measurableSet.inter ?_
      refine MeasurableSet.iInter fun s => ?_
      exact MeasurableSet.iInter fun hs => (q_meas _).diff (q_meas _)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
γ : Type u_3
β : Type u_4
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst, inst_2] f
f_inj : Injective f
this_1 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this_2 : Encodable (↑b : Type u_3)
A : Type (max 0 u_3) := { p : (↑b : Type u_3) × (↑b : Type u_3) // Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ) }
q : (p : A) → Set β
hq1 : ∀ (p : A), f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ) ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ)) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : (↑b : Type u_3) → Set β :=
  fun (s : (↑b : Type u_3)) ↦
    closure[inst_2] (f '' (↑s : Set γ)) ∩
      ⋂ (t : (↑b : Type u_3)),
        ⋂ (ht : Disjoint (↑s : Set γ) (↑t : Set γ)),
          q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (s, t) ht) \
            q
              (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
                (t, s) ⋯)
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β :=
  fun (n : ℕ) ↦ ⋃ (s : (↑b : Type u_3)), ⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s
this : range f = ⋂ (n : ℕ), F n
E_meas : ∀ (s : (↑b : Type u_3)), MeasurableSet (E s)
n : ℕ
⊢ MeasurableSet (F n)

Tactic:
MeasurableSet.iUnion fun s => ?_

Premises used: MeasurableSet.iUnion