awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
refine_1 : f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n ⊆ u
refine_2 : Disjoint (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n) u
⊢ MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n)

Tactic:
refine ⟨u, ?_, ?_, u_open.measurableSet⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
refine_1 : cylinder (E := fun (a : ℕ) ↦ ℕ) x n ⊆ f ⁻¹' u
⊢ f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n ⊆ u

Tactic:
rw [image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
apply : cylinder (E := fun (a : ℕ) ↦ ℕ) x n ⊆ ball x εx
⊢ cylinder (E := fun (a : ℕ) ↦ ℕ) x n ⊆ f ⁻¹' u

Tactic:
apply Subset.trans _ hεx

Premises used: Set.Subset.trans
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : ℕ) ↦ ℕ) x n
⊢ dist z x ≤ (1 / 2) ^ n

Tactic:
rw [mem_cylinder_iff_dist_le] at hz

Premises used: PiNat.mem_cylinder_iff_dist_le
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : dist z x ≤ (1 / 2) ^ n
⊢ z ∈ ball x εx

Tactic:
hz.trans_lt (hn.trans_le (min_le_left _ _))

Premises used: Set.Mem, setOf, Metric.ball, min_le_left, LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : dist z x ≤ (1 / 2) ^ n
⊢ z ∈ ball x εx

Tactic:
exact hz.trans_lt (hn.trans_le (min_le_left _ _))

Premises used: min_le_left, LT.lt.trans_le, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ Disjoint (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n) u

Tactic:
Disjoint.mono_left ?_ huv.symm

Premises used: Disjoint.mono_left, Disjoint.symm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
refine_2 : g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n ≤ v
⊢ Disjoint (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n) u

Tactic:
refine Disjoint.mono_left ?_ huv.symm

Premises used: Disjoint.mono_left, Disjoint.symm