-- 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
⊢ False
have B : MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y n)
Tactic: have B : MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) := by
    refine ⟨u, ?_, ?_, u_open.measurableSet⟩
    · rw [image_subset_iff]
      apply Subset.trans _ hεx
      intro z hz
      rw [mem_cylinder_iff_dist_le] at hz
      exact hz.trans_lt (hn.trans_le (min_le_left _ _))
    · refine Disjoint.mono_left ?_ huv.symm
      change g '' cylinder y n ⊆ v
      rw [image_subset_iff]
      apply Subset.trans _ hεy
      intro z hz
      rw [mem_cylinder_iff_dist_le] at hz
      exact hz.trans_lt (hn.trans_le (min_le_right _ _))