awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst] f
hg : Continuous[_, inst] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : (n : ℕ) → ℕ),
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n) →
      ∃ (x' : (n : ℕ) → ℕ) (y' : (n : ℕ) → ℕ),
        x' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) x n ∧
          y' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) y n ∧
            ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x' (n + 1))
                (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y' (n + 1))
A : Type :=
  { p : ℕ × (ℕ → ℕ) × (ℕ → ℕ) //
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.1 p.1)
        (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.2 p.1) }
F : (p : A) → A
hFn : ∀ (p : A), (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 + 1
hFx :
  ∀ (p : A),
    (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
      cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
hFy :
  ∀ (p : A),
    (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
      cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
p0 : A :=
  Subtype.mk (p := fun (p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)) ↦
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.1 p.1)
        (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.2 p.1))
    (0, fun (x : ℕ) ↦ 0, fun (x : ℕ) ↦ 0) ⋯
p : ℕ → A := fun (n : ℕ) ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 m
x : ℕ → ℕ := fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 n
hx : x = fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 n
y : ℕ → ℕ := fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 n
hy : y = fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 n
M :
  ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n)
u v : Set α
u_open : IsOpen[inst] u
v_open : IsOpen[inst] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
εx : ℝ
εxpos : εx > 0
hεx : ball x εx ⊆ f ⁻¹' u
εy : ℝ
εypos : εy > 0
hεy : ball y εy ⊆ g ⁻¹' v
n : ℕ
hn : (1 / 2) ^ n < min εx εy
⊢ g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n ⊆ v
have refine_2 : cylinder (E := fun (a : ℕ) ↦ ℕ) y n ⊆ g ⁻¹' v
Tactic: rw [image_subset_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst] f
hg : Continuous[_, inst] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : (n : ℕ) → ℕ),
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n) →
      ∃ (x' : (n : ℕ) → ℕ) (y' : (n : ℕ) → ℕ),
        x' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) x n ∧
          y' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) y n ∧
            ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x' (n + 1))
                (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y' (n + 1))
A : Type :=
  { p : ℕ × (ℕ → ℕ) × (ℕ → ℕ) //
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.1 p.1)
        (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.2 p.1) }
F : (p : A) → A
hFn : ∀ (p : A), (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 + 1
hFx :
  ∀ (p : A),
    (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
      cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
hFy :
  ∀ (p : A),
    (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
      cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
p0 : A :=
  Subtype.mk (p := fun (p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)) ↦
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.1 p.1)
        (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.2 p.1))
    (0, fun (x : ℕ) ↦ 0, fun (x : ℕ) ↦ 0) ⋯
p : ℕ → A := fun (n : ℕ) ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 m
x : ℕ → ℕ := fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 n
hx : x = fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 n
y : ℕ → ℕ := fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 n
hy : y = fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 n
M :
  ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n)
u v : Set α
u_open : IsOpen[inst] u
v_open : IsOpen[inst] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
εx : ℝ
εxpos : εx > 0
hεx : ball x εx ⊆ f ⁻¹' u
εy : ℝ
εypos : εy > 0
hεy : ball y εy ⊆ g ⁻¹' v
n : ℕ
hn : (1 / 2) ^ n < min εx εy
⊢ cylinder (E := fun (a : ℕ) ↦ ℕ) y n ⊆ g ⁻¹' v
have apply : cylinder (E := fun (a : ℕ) ↦ ℕ) y n ⊆ ball y εy
Tactic: apply Subset.trans _ hεy
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
f g : (ℕ → ℕ) → α
hf : Continuous[_, inst] f
hg : Continuous[_, inst] g
h : Disjoint (range f) (range g)
hfg : ¬MeasurablySeparable (range f) (range g)
I :
  ∀ (n : ℕ) (x y : (n : ℕ) → ℕ),
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n) →
      ∃ (x' : (n : ℕ) → ℕ) (y' : (n : ℕ) → ℕ),
        x' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) x n ∧
          y' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) y n ∧
            ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x' (n + 1))
                (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y' (n + 1))
A : Type :=
  { p : ℕ × (ℕ → ℕ) × (ℕ → ℕ) //
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.1 p.1)
        (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.2 p.1) }
F : (p : A) → A
hFn : ∀ (p : A), (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 + 1
hFx :
  ∀ (p : A),
    (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
      cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
hFy :
  ∀ (p : A),
    (↑(F p) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
      cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
p0 : A :=
  Subtype.mk (p := fun (p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)) ↦
    ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.1 p.1)
        (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) p.2.2 p.1))
    (0, fun (x : ℕ) ↦ 0, fun (x : ℕ) ↦ 0) ⋯
p : ℕ → A := fun (n : ℕ) ↦ F^[n] p0
prec : ∀ (n : ℕ), p (n + 1) = F (p n)
pn_fst : ∀ (n : ℕ), (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n
Ix : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
Iy : ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 m
x : ℕ → ℕ := fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 n
hx : x = fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 n
y : ℕ → ℕ := fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 n
hy : y = fun (n : ℕ) ↦ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 n
M :
  ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n)
u v : Set α
u_open : IsOpen[inst] u
v_open : IsOpen[inst] v
xu : f x ∈ u
yv : g y ∈ v
huv : Disjoint u v
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
εx : ℝ
εxpos : εx > 0
hεx : ball x εx ⊆ f ⁻¹' u
εy : ℝ
εypos : εy > 0
hεy : ball y εy ⊆ g ⁻¹' v
n : ℕ
hn : (1 / 2) ^ n < min εx εy
z : ℕ → ℕ
hz : z ∈ cylinder (E := fun (a : ℕ) ↦ ℕ) y n
⊢ z ∈ ball y εy
have hz₁ : dist z y ≤ (1 / 2) ^ n
Tactic: rw [mem_cylinder_iff_dist_le] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s t : Set α
hs : AnalyticSet s
ht : AnalyticSet t
h : Disjoint s t
⊢ MeasurablySeparable s t
have hs₁ : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
Tactic: rw [AnalyticSet] at hs ht
Cleared hypotheses: hs, ht, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s t : Set α
hs : AnalyticSet s
ht : AnalyticSet t
h : Disjoint s t
hs₁ : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
⊢ MeasurablySeparable s t
have ht₁ : t = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = t
Tactic: rw [AnalyticSet] at hs ht
Cleared hypotheses: hs, ht, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
ht : t = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t
have inl : ∀ (h : Disjoint ∅ t), MeasurablySeparable ∅ t
Tactic: rcases hs with (rfl | ⟨f, f_cont, rfl⟩)
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s
ht : t = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = t
h : Disjoint s t
inl : ∀ (h : Disjoint ∅ t), MeasurablySeparable ∅ t
⊢ MeasurablySeparable s t
have inr : ∀ (f : (ℕ → ℕ) → α) (f_cont : Continuous[_, inst] f) (h : Disjoint (range f) t), MeasurablySeparable (range f) t
Tactic: rcases hs with (rfl | ⟨f, f_cont, rfl⟩)
Cleared hypotheses: s, hs, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = t
f : (ℕ → ℕ) → α
f_cont : Continuous[_, inst] f
h : Disjoint (range f) t
⊢ MeasurablySeparable (range f) t
have inr : ∀ (h : Disjoint (range f) ∅), MeasurablySeparable (range f) ∅
Tactic: rcases ht with (rfl | ⟨g, g_cont, rfl⟩)
Cleared hypotheses: t, ht, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = t
f : (ℕ → ℕ) → α
f_cont : Continuous[_, inst] f
h : Disjoint (range f) t
inr : ∀ (h : Disjoint (range f) ∅), MeasurablySeparable (range f) ∅
⊢ MeasurablySeparable (range f) t
have inr₁ : ∀ (g : (ℕ → ℕ) → α) (g_cont : Continuous[_, inst] g) (h : Disjoint (range f) (range g)),
  MeasurablySeparable (range f) (range g)
Tactic: rcases ht with (rfl | ⟨g, g_cont, rfl⟩)
Cleared hypotheses: t, ht, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
⊢ MeasurableSet s
have rcases : ∀ (u : Set α) (hsu : s ⊆ u) (hdu : Disjoint sᶜ u) (hmu : MeasurableSet u), MeasurableSet s
Tactic: rcases hs.measurablySeparable hsc disjoint_compl_right with ⟨u, hsu, hdu, hmu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
⊢ MeasurableSet s
have hsu₁ : s ⊆ s
Tactic: obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)
Cleared hypotheses: u, hsu, hdu, hmu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
s : Set α
hs : AnalyticSet s
hsc : AnalyticSet sᶜ
u : Set α
hsu : s ⊆ u
hdu : Disjoint sᶜ u
hmu : MeasurableSet u
hsu₁ : s ⊆ s
⊢ MeasurableSet s
have hdu₁ : Disjoint sᶜ s
Tactic: obtain rfl : s = u := hsu.antisymm (disjoint_compl_left_iff_subset.1 hdu)
Cleared hypotheses: u, hsu, hdu, hmu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet s
have refine : ∀ (h : MeasurableSet (f ⁻¹' s)), MeasurableSet s
Tactic: refine ⟨fun h => ?_, fun h => hf h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
⊢ MeasurableSet s
have rcases : ∀ (τ : TopologicalSpace Z), SecondCountableTopology Z → T4Space Z → OpensMeasurableSpace Z → MeasurableSet s
Tactic: rcases exists_opensMeasurableSpace_of_countablySeparated Z with ⟨τ, _, _, _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ MeasurableSet s
have hs : AnalyticSet s
Tactic: apply AnalyticSet.measurableSet_of_compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
hs : AnalyticSet s
⊢ MeasurableSet s
have hsc : AnalyticSet sᶜ
Tactic: apply AnalyticSet.measurableSet_of_compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ AnalyticSet s
have hs : AnalyticSet (f '' f ⁻¹' s)
Tactic: rw [← image_preimage_eq s hsurj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
inst_3 : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left : SecondCountableTopology Z
left_1 : T4Space Z
right : OpensMeasurableSpace Z
⊢ AnalyticSet sᶜ
have hsc : AnalyticSet (f '' f ⁻¹' sᶜ)
Tactic: rw [← image_preimage_eq sᶜ hsurj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst = borel Y
have d : Measurable f
Tactic: have d := hf.mono le_rfl OpensMeasurableSpace.borel_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
this : MeasurableSpace Y := borel Y
⊢ MeasurableSpace.map f inst = borel Y
have this₁ : BorelSpace Y
Tactic: haveI : BorelSpace Y := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
f : X → Z
inst_3 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
have rw : MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
  MeasurableSet (s ∩ range f)
Tactic: rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
    ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
f : X → Z
inst_3 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
rw :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (s ∩ range f)
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
have rw₁ : MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
  MeasurableSet (range f ∩ s)
Tactic: rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
    ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
f : X → Z
inst_3 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
rw :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (s ∩ range f)
rw₁ :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (range f ∩ s)
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
have rw₂ : MeasurableSet
    (image (α := { x : Z // x ∈ range f }) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f))
      (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s)) ↔
  MeasurableSet (range f ∩ s)
Tactic: rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
    ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Z : Type u_5
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : MeasurableSpace Z
f : X → Z
inst_3 : CountablySeparated.{u_5} (↑(range f) : Type u_5)
hf : Measurable f
hr : MeasurableSet (range f)
s : Set Z
rw :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (s ∩ range f)
rw₁ :
  MeasurableSet (α := (↑(range f) : Type u_5)) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s) ↔
    MeasurableSet (range f ∩ s)
rw₂ :
  MeasurableSet
      (image (α := { x : Z // x ∈ range f }) (Subtype.val (p := fun (x : Z) ↦ x ∈ range f))
        (Subtype.val (p := fun (x : Z) ↦ x ∈ range f) ⁻¹' s)) ↔
    MeasurableSet (range f ∩ s)
⊢ MeasurableSet (f ⁻¹' s) ↔ MeasurableSet (s ∩ range f)
have rw₃ : MeasurableSet (range f ∩ s) ↔ MeasurableSet (range f ∩ s)
Tactic: rw [hf.measurableSet_preimage_iff_preimage_val, inter_comm,
    ← (MeasurableEmbedding.subtype_coe hr).measurableSet_image, Subtype.image_preimage_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : TopologicalSpace Y
inst_5 : T0Space Y
inst_6 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_4] f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst_2 = borel Y
have this : let this := borel Y;
BorelSpace Y
Tactic: borelize Y
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : PolishSpace X
inst_2 : TopologicalSpace Y
inst_3 : T0Space Y
inst_4 : SecondCountableTopology Y
f : X → Y
hf : Continuous[inst, inst_2] f
hsurj : Surjective f
⊢ MeasurableSpace.map f (borel X) = borel Y
have this : let this := borel X;
BorelSpace X
Tactic: borelize X
-- 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 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
⊢ MeasurableSet (range f)
have obtain : ∀ (b : Set (Set γ)) (b_count : b.Countable) (b_nonempty : ∅ ∉ b) (hb : IsTopologicalBasis b), MeasurableSet (range f)
Tactic: obtain ⟨b, b_count, b_nonempty, hb⟩ :
    ∃ b : Set (Set γ), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b := exists_countable_basis γ
-- 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 : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
⊢ MeasurableSet (range f)
have haveI : ∀ (this : Encodable (↑b : Type u_3)), MeasurableSet (range f)
Tactic: haveI : Encodable b := b_count.toEncodable
-- 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 γ) }
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
have this₁ : Disjoint (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).1 : Set γ))
  (f '' (↑(↑p : (↑b : Type u_3) × (↑b : Type u_3)).2 : Set γ))
Tactic: apply
      AnalyticSet.measurablySeparable ((hb.isOpen p.1.1.2).analyticSet_image f_cont)
        ((hb.isOpen p.1.2.2).analyticSet_image f_cont)