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
n : ℕ
⊢ cylinder (E := fun (a : ℕ) ↦ ℕ) x n =
    cylinder (E := fun (a : ℕ) ↦ ℕ) (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
have h₁ : ∀ i < n, x i = (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 i
Tactic: rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_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
n : ℕ
⊢ cylinder (E := fun (a : ℕ) ↦ ℕ) y n =
    cylinder (E := fun (a : ℕ) ↦ ℕ) (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
have h₁ : ∀ i < n, y i = (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 i
Tactic: rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
-- 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
⊢ False
have M : ∀ (n : ℕ), ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n)
Tactic: have M : ∀ n, ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) := by
    intro n
    convert! (p n).2 using 3
    · rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
      intro i hi
      rw [hx]
      exact (Ix i n hi).symm
    · rw [pn_fst, ← mem_cylinder_iff_eq, mem_cylinder_iff]
      intro i hi
      rw [hy]
      exact (Iy i n hi).symm
-- 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 : Set α) (v : Set α), IsOpen[inst] u ∧ IsOpen[inst] v ∧ f x ∈ u ∧ g y ∈ v ∧ Disjoint u v
have h₁ : f x ≠ g y
Tactic: apply t2_separation
-- 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)
⊢ False
have obtain : ∀ (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),
  False
Tactic: obtain ⟨u, v, u_open, v_open, xu, yv, huv⟩ :
      ∃ u v : Set α, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ g y ∈ v ∧ Disjoint u v := by
    apply t2_separation
    exact disjoint_iff_forall_ne.1 h (mem_range_self _) (mem_range_self _)
-- 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 > 0, ball x εx ⊆ f ⁻¹' u
have apply : f ⁻¹' u ∈ 𝓝 x
Tactic: apply Metric.mem_nhds_iff.1
-- 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
⊢ False
have obtain : ∀ (εx : ℝ) (εxpos : εx > 0) (hεx : ball x εx ⊆ f ⁻¹' u), False
Tactic: obtain ⟨εx, εxpos, hεx⟩ : ∃ (εx : ℝ), εx > 0 ∧ Metric.ball x εx ⊆ f ⁻¹' u := by
    apply Metric.mem_nhds_iff.1
    exact hf.continuousAt.preimage_mem_nhds (u_open.mem_nhds xu)
-- 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 > 0, ball y εy ⊆ g ⁻¹' v
have apply : g ⁻¹' v ∈ 𝓝 y
Tactic: apply Metric.mem_nhds_iff.1