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 γ) }
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
y : γ
n : ℕ
⊢ ball y (u n / 2) ∈ 𝓝 y

Tactic:
exact ball_mem_nhds _ (half_pos (u_pos n))

Premises used: half_pos, Metric.ball_mem_nhds
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
h₁ : ∀ (s : Set γ) (sb : s ∈ b) (ys : y ∈ s) (hs : s ⊆ ball y (u n / 2)), f y ∈ F n
⊢ f y ∈ F n

Tactic:
obtain ⟨s, sb, ys, hs⟩ : ∃ (s : Set γ), s ∈ b ∧ y ∈ s ∧ s ⊆ ball y (u n / 2) := by
      apply hb.mem_nhds_iff.1
      exact ball_mem_nhds _ (half_pos (u_pos n))

Premises used: HDiv.hDiv, Metric.ball, OfNat.ofNat, Set
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
apply : diam (ball y (u n / 2)) ≤ u n
⊢ diam s ≤ u n

Tactic:
apply (diam_mono hs isBounded_ball).trans

Premises used: Metric.isBounded_ball, Metric.diam_mono, LE.le.trans
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
⊢ diam (ball y (u n / 2)) ≤ 2 * (u n / 2)

Tactic:
diam_ball (x := y) (half_pos (u_pos n)).le

Premises used: half_pos, LT.lt.le, Metric.diam_ball
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
h : u n = 2 * (u n / 2)
⊢ diam (ball y (u n / 2)) ≤ u n

Tactic:
convert! diam_ball (x := y) (half_pos (u_pos n)).le

Premises used: half_pos, LT.lt.le, Metric.diam_ball
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
⊢ u n = 2 * (u n / 2)

Tactic:
ring
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
⊢ diam s ≤ u n

Tactic:
have diam_s : diam s ≤ u n := by
      apply (diam_mono hs isBounded_ball).trans
      convert! diam_ball (x := y) (half_pos (u_pos n)).le
      ring
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
⊢ f y ∈ F n

Tactic:
mem_iUnion.2 ⟨⟨s, sb⟩, ?_⟩

Premises used: Iff.mpr, Set.Mem, Set.mem_iUnion, Subtype.mk, Exists.intro
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
h₁ :
  Membership.mem (γ := Set β)
    (⋃ (_ :
      Bornology.IsBounded (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) ∧
        diam (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) ≤ u n),
      E (Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb))
    (f y)
⊢ f y ∈ F n

Tactic:
refine mem_iUnion.2 ⟨⟨s, sb⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
⊢ Membership.mem (γ := Set β)
    (⋃ (_ :
      Bornology.IsBounded (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) ∧
        diam (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) ≤ u n),
      E (Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb))
    (f y)

Tactic:
mem_iUnion.2 ⟨⟨isBounded_ball.subset hs, diam_s⟩, ?_⟩

Premises used: Metric.isBounded_ball, Iff.mpr, Set.mem_iUnion, Bornology.IsBounded.subset, And.intro, Exists.intro
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
h₁ : f y ∈ E (Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb)
⊢ Membership.mem (γ := Set β)
    (⋃ (_ :
      Bornology.IsBounded (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) ∧
        diam (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) ≤ u n),
      E (Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb))
    (f y)

Tactic:
refine mem_iUnion.2 ⟨⟨isBounded_ball.subset hs, diam_s⟩, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- 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 : ℕ → ℝ
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
y : γ
n : ℕ
s : Set γ
sb : s ∈ b
ys : y ∈ s
hs : s ⊆ ball y (u n / 2)
diam_s : diam s ≤ u n
h₁ :
  Membership.mem (γ := Set β)
    (⋂ (t : (↑b : Type u_3)),
      ⋂ (ht : Disjoint (↑(Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) : Set γ) (↑t : Set γ)),
        q
            (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb, t) ht) \
          q
            (Subtype.mk (p := fun (p : (↑b : Type u_3) × (↑b : Type u_3)) ↦ Disjoint (↑p.1 : Set γ) (↑p.2 : Set γ))
              (t, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb) ⋯))
    (f y)
⊢ f y ∈ E (Subtype.mk (p := fun (x : Set γ) ↦ x ∈ b) s sb)

Tactic:
apply mem_inter (subset_closure (mem_image_of_mem _ ys))

Premises used: subset_closure, Set.mem_inter, Set.mem_image_of_mem