awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
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 γ) }
⊢ MeasurableSet (range f)
have 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
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 _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ MeasurableSet (range f)
have 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)
Tactic: choose q hq1 hq2 q_meas using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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) ⋯)
⊢ MeasurableSet (range f)
have obtain : ∀ (u : ℕ → ℝ) (u_anti : StrictAnti u) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)),
  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 : ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
have 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) sorry))
Tactic: refine isClosed_closure.measurableSet.inter ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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) ⋯))
have 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) sorry))
Tactic: refine MeasurableSet.iInter fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
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
⊢ MeasurableSet (range f)
have E_meas : ∀ (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 _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
have refine : ∀ (s : (↑b : Type u_3)),
  MeasurableSet.{u_4} (α := β) (⋃ (_ : Bornology.IsBounded (↑s : Set γ) ∧ diam (↑s : Set γ) ≤ u n), E s)
Tactic: refine MeasurableSet.iUnion fun s => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
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)
⊢ MeasurableSet (range f)
have F_meas : ∀ (n : ℕ), MeasurableSet (F n)
Tactic: have F_meas : ∀ n, MeasurableSet (F n) := by
      intro n
      refine MeasurableSet.iUnion fun s => ?_
      exact MeasurableSet.iUnion fun _ => E_meas _
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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)
F_meas : ∀ (n : ℕ), MeasurableSet (F n)
⊢ MeasurableSet (range f)
have rw : MeasurableSet.{u_4} (α := β) (⋂ (n : ℕ), F n)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ MeasurableSet (range f)
have suffices : range f = ⋂ (n : ℕ), F n
Tactic: suffices range f = ⋂ n, F n by
    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 _)
    have F_meas : ∀ n, MeasurableSet (F n) := by
      intro n
      refine MeasurableSet.iUnion fun s => ?_
      exact MeasurableSet.iUnion fun _ => E_meas _
    rw [this]
    exact MeasurableSet.iInter fun n => F_meas n
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
⊢ range f = ⋂ (n : ℕ), F n
have h₁ : range f ⊆ ⋂ (n : ℕ), F n
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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
h₁ : range f ⊆ ⋂ (n : ℕ), F n
⊢ range f = ⋂ (n : ℕ), F n
have h₂ : ⋂ (n : ℕ), F n ⊆ range f
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
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 : γ
⊢ Membership.mem (γ := Set β) (⋂ (n : ℕ), F n) (f y)
have h₁ : ∀ (n : ℕ), f y ∈ F n
Tactic: refine mem_iInter.2 fun n => ?_