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)
n : ℕ
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n
⊢ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n + 1

Tactic:
simp only [prec, hFn, IH]
-- 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)
n : ℕ
zero : (↑(p 0) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = 0
succ : ∀ (n : ℕ) (IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n), (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n + 1
⊢ (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n

Tactic:
induction n with
    | zero => rfl
    | succ n IH => simp only [prec, hFn, IH]
-- 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)
⊢ ∀ (n : ℕ), (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n

Tactic:
have pn_fst : ∀ n, (p n).1.1 = n := fun n ↦ by
    induction n with
    | zero => rfl
    | succ n IH => simp only [prec, hFn, IH]
-- 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
m : ℕ
base : (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
succ :
  ∀ (n : ℕ) (hmn : m + 1 ≤ n),
    (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m →
      (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
⊢ ∀ (n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m

Tactic:
apply Nat.le_induction
-- 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
m : ℕ
⊢ (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m

Tactic:
rfl
-- 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
apply : m < (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
⊢ (↑(F (p n)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m

Tactic:
apply hFx (p n) m
-- 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
rw : m < n
⊢ m < (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1

Tactic:
rw [pn_fst]
-- 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
⊢ m < n

Tactic:
hmn

Premises used: Nat.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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
⊢ m < n

Tactic:
exact hmn
-- 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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
⊢ (↑(F (p n)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m

Tactic:
have I : (F (p n)).val.snd.fst m = (p n).val.snd.fst m := by
      apply hFx (p n) m
      rw [pn_fst]
      exact hmn
-- 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_1 :
  ∀ (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
m n : ℕ
hmn : m + 1 ≤ n
IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
I : (↑(F (p n)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
succ : (↑(F (p n)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
succ₁ : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
succ₂ succ₃ : (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m
⊢ (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m

Tactic:
rw [prec, I, IH]
-- 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
⊢ ∀ (m n : ℕ), m + 1 ≤ n → (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m = (↑(p (m + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 m

Tactic:
have Ix : ∀ m n, m + 1 ≤ n → (p n).1.2.1 m = (p (m + 1)).1.2.1 m := by
    intro m
    apply Nat.le_induction
    · rfl
    intro n hmn IH
    have I : (F (p n)).val.snd.fst m = (p n).val.snd.fst m := by
      apply hFx (p n) m
      rw [pn_fst]
      exact hmn
    rw [prec, I, IH]