-- 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) }
n : ℕ
x y : ℕ → ℕ
hp :
  ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) (n, x, y).2.1 (n, x, y).1)
      (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) (n, x, y).2.2 (n, x, y).1)
rcases :
  ∀ (x' y' : (n : ℕ) → ℕ) (hx' : x' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) x n)
    (hy' : y' ∈ cylinder (E := fun (n : ℕ) ↦ ℕ) y n)
    (h' :
      ¬MeasurablySeparable (f '' cylinder (E := fun (a : ℕ) ↦ ℕ) x' (n + 1))
          (g '' cylinder (E := fun (a : ℕ) ↦ ℕ) y' (n + 1))),
    ∃ (q : A),
      (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 =
          (↑(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))
                    (n, x, y) hp) :
                ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 +
            1 ∧
        (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
            cylinder (E := fun (n : ℕ) ↦ ℕ)
              (↑(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))
                        (n, x, y) hp) :
                    ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1
              (↑(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))
                      (n, x, y) hp) :
                  ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 ∧
          (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
            cylinder (E := fun (n : ℕ) ↦ ℕ)
              (↑(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))
                        (n, x, y) hp) :
                    ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2
              (↑(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))
                      (n, x, y) hp) :
                  ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
⊢ ∃ (q : A),
    (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 =
        (↑(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))
                  (n, x, y) hp) :
              ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 +
          1 ∧
      (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
          cylinder (E := fun (n : ℕ) ↦ ℕ)
            (↑(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))
                      (n, x, y) hp) :
                  ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1
            (↑(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))
                    (n, x, y) hp) :
                ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 ∧
        (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
          cylinder (E := fun (n : ℕ) ↦ ℕ)
            (↑(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))
                      (n, x, y) hp) :
                  ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2
            (↑(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))
                    (n, x, y) hp) :
                ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1

Tactic:
rcases I n x y hp with ⟨x', y', hx', hy', h'⟩