awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
⊢ AnalyticSet (f '' s)
have rcases : ∀ (τ' : TopologicalSpace X) (hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace) (hfc : Continuous[_, inst_2] f)
  (hτ' : PolishSpace X), AnalyticSet (f '' s)
Tactic: rcases hf.exists_continuous with ⟨τ', hle, hfc, hτ'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous[τ', inst_2] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
⊢ AnalyticSet (f '' s)
have b' : BorelSpace X
Tactic: haveI b' : BorelSpace X := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : MeasurableSpace X
inst_1 : StandardBorelSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace Y
inst_4 : OpensMeasurableSpace Y
f : X → Y
inst_5 : SecondCountableTopology.{u_4} (↑(range f) : Type u_4)
s : Set X
hs : MeasurableSet s
hf : Measurable f
this : UpgradedStandardBorel X := upgradeStandardBorel X
τ' : TopologicalSpace X
hle : τ' ≤ UpgradedStandardBorel.toTopologicalSpace
hfc : Continuous[τ', inst_2] f
hτ' : PolishSpace X
m' : MeasurableSpace X := borel X
b' : BorelSpace X
⊢ AnalyticSet (f '' s)
have hle₁ : borel X ≤ borel X
Tactic: have hle := borel_anti hle
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
s : Set Y
hs : AnalyticSet s
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ AnalyticSet (f ⁻¹' s)
have rcases : ∀ (Z : Type) (w : TopologicalSpace Z),
  PolishSpace Z → ∀ (g : Z → Y) (hg : Continuous[_, inst_1] g) (hs : AnalyticSet (range g)), AnalyticSet (f ⁻¹' range g)
Tactic: rcases analyticSet_iff_exists_polishSpace_range.1 hs with ⟨Z, _, _, g, hg, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
⊢ AnalyticSet (f ⁻¹' range g)
have this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
Tactic: have : IsClosed {x : X × Z | f x.1 = g x.2} := isClosed_eq hf.fst' hg.snd'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
⊢ AnalyticSet (f ⁻¹' range g)
have h : f ⁻¹' range g = image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}
Tactic: convert! this.analyticSet.image_of_continuous continuous_fst
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
X : Type u_3
Y : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : PolishSpace X
inst_3 : T2Space Y
f : X → Y
hf : Continuous[inst, inst_1] f
Z : Type
w : TopologicalSpace Z
w_1 : PolishSpace Z
g : Z → Y
hg : Continuous[w, inst_1] g
hs : AnalyticSet (range g)
this : IsClosed[instTopologicalSpaceProd] {x : X × Z | f x.1 = g x.2}
⊢ f ⁻¹' range g = image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}
have h : ∀ (x : X), x ∈ f ⁻¹' range g ↔ Membership.mem (γ := Set X) (image (α := X × Z) Prod.fst {x : X × Z | f x.1 = g x.2}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
h : ∀ (m n : ι), MeasurablySeparable (s m) (t n)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)
have choose : ∀ (u : (m n : ι) → Set α) (hsu : ∀ (m n : ι), s m ⊆ u m n) (htu : ∀ (m n : ι), Disjoint (t n) (u m n))
  (hu : ∀ (m n : ι), MeasurableSet (u m n)), MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)
Tactic: choose u hsu htu hu using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)
have refine_1 : Subset.{u_3} (α := Set α) (⋃ (n : ι), s n) (⋃ (m : ι), ⋂ (n : ι), u m n)
Tactic: refine ⟨⋃ m, ⋂ n, u m n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
refine_1 : Subset.{u_3} (α := Set α) (⋃ (n : ι), s n) (⋃ (m : ι), ⋂ (n : ι), u m n)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)
have refine_2 : Disjoint.{u_3} (α := Set α) (⋃ (m : ι), t m) (⋃ (m : ι), ⋂ (n : ι), u m n)
Tactic: refine ⟨⋃ m, ⋂ n, u m n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
refine_1 : Subset.{u_3} (α := Set α) (⋃ (n : ι), s n) (⋃ (m : ι), ⋂ (n : ι), u m n)
refine_2 : Disjoint.{u_3} (α := Set α) (⋃ (m : ι), t m) (⋃ (m : ι), ⋂ (n : ι), u m n)
⊢ MeasurablySeparable.{u_3} (α := α) (⋃ (n : ι), s n) (⋃ (m : ι), t m)
have refine_3 : MeasurableSet.{u_3} (α := α) (⋃ (m : ι), ⋂ (n : ι), u m n)
Tactic: refine ⟨⋃ m, ⋂ n, u m n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Subset.{u_3} (α := Set α) (⋃ (n : ι), s n) (⋃ (m : ι), ⋂ (n : ι), u m n)
have refine_1 : ∀ (m : ι), s m ⊆ ⋂ (n : ι), u m n
Tactic: refine iUnion_subset fun m => subset_iUnion_of_subset m ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ Disjoint.{u_3} (α := Set α) (⋃ (m : ι), t m) (⋃ (m : ι), ⋂ (n : ι), u m n)
have refine_2 : ∀ (i i_1 : ι), Disjoint (t i) (⋂ (n : ι), u i_1 n)
Tactic: simp_rw [disjoint_iUnion_left, disjoint_iUnion_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
n m : ι
⊢ Disjoint (t n) (⋂ (n : ι), u m n)
have apply : ⋂ (n : ι), u m n ≤ u m n
Tactic: apply Disjoint.mono_right _ (htu m n)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
inst : Countable ι
α : Type u_3
inst_1 : MeasurableSpace α
s t : ι → Set α
u : (m n : ι) → Set α
hsu : ∀ (m n : ι), s m ⊆ u m n
htu : ∀ (m n : ι), Disjoint (t n) (u m n)
hu : ∀ (m n : ι), MeasurableSet (u m n)
⊢ MeasurableSet.{u_3} (α := α) (⋃ (m : ι), ⋂ (n : ι), u m n)
have refine_3 : ∀ (m : ι), MeasurableSet.{u_3} (α := α) (⋂ (n : ι), u m n)
Tactic: refine MeasurableSet.iUnion fun m => ?_
-- 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)
⊢ MeasurablySeparable (range f) (range g)
have by_contra : ∀ (hfg : ¬MeasurablySeparable (range f) (range g)), False
Tactic: by_contra hfg
-- 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)
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))
have contrapose! : (∀ (x' 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))) →
  MeasurablySeparable (f '' cylinder (E := fun (n : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (n : ℕ) ↦ ℕ) y n)
Tactic: contrapose!
-- 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)
n : ℕ
x y : (n : ℕ) → ℕ
H :
  ∀ (x' 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))
⊢ MeasurablySeparable (f '' cylinder (E := fun (n : ℕ) ↦ ℕ) x n) (g '' cylinder (E := fun (n : ℕ) ↦ ℕ) y n)
have rw : MeasurablySeparable.{u_1} (α := α)
  (⋃ (i : ℕ), f '' cylinder (E := fun (n : ℕ) ↦ ℕ) (update (β := fun (n : ℕ) ↦ ℕ) x n i) (n + 1))
  (⋃ (i : ℕ), g '' cylinder (E := fun (n : ℕ) ↦ ℕ) (update (β := fun (n : ℕ) ↦ ℕ) y n i) (n + 1))
Tactic: rw [← iUnion_cylinder_update x n, ← iUnion_cylinder_update y n, image_iUnion, image_iUnion]
-- 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)
n : ℕ
x y : (n : ℕ) → ℕ
H :
  ∀ (x' 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))
⊢ MeasurablySeparable.{u_1} (α := α)
    (⋃ (i : ℕ), f '' cylinder (E := fun (n : ℕ) ↦ ℕ) (update (β := fun (n : ℕ) ↦ ℕ) x n i) (n + 1))
    (⋃ (i : ℕ), g '' cylinder (E := fun (n : ℕ) ↦ ℕ) (update (β := fun (n : ℕ) ↦ ℕ) y n i) (n + 1))
have refine : ∀ (i j : ℕ),
  MeasurablySeparable (f '' cylinder (E := fun (n : ℕ) ↦ ℕ) (update (β := fun (n : ℕ) ↦ ℕ) x n i) (n + 1))
    (g '' cylinder (E := fun (n : ℕ) ↦ ℕ) (update (β := fun (n : ℕ) ↦ ℕ) y n j) (n + 1))
Tactic: refine MeasurablySeparable.iUnion fun i j => ?_
-- 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)
⊢ False
have 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))
Tactic: have I : ∀ n x y, ¬MeasurablySeparable (f '' cylinder x n) (g '' cylinder y n) →
      ∃ x' y', x' ∈ cylinder x n ∧ y' ∈ cylinder y n ∧
      ¬MeasurablySeparable (f '' cylinder x' (n + 1)) (g '' cylinder y' (n + 1)) := by
    intro n x y
    contrapose!
    intro H
    rw [← iUnion_cylinder_update x n, ← iUnion_cylinder_update y n, image_iUnion, image_iUnion]
    refine MeasurablySeparable.iUnion fun i j => ?_
    exact H _ _ (update_mem_cylinder _ _ _) (update_mem_cylinder _ _ _)
-- 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) }
⊢ False
have this : ∀ (p : A),
  ∃ (q : A),
    (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 + 1 ∧
      (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
          cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 ∧
        (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
          cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
Tactic: have : ∀ p : A, ∃ q : A,
      q.1.1 = p.1.1 + 1 ∧ q.1.2.1 ∈ cylinder p.1.2.1 p.1.1 ∧ q.1.2.2 ∈ cylinder p.1.2.2 p.1.1 := by
    rintro ⟨⟨n, x, y⟩, hp⟩
    rcases I n x y hp with ⟨x', y', hx', hy', h'⟩
    exact ⟨⟨⟨n + 1, x', y'⟩, h'⟩, rfl, hx', hy'⟩
-- 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) }
this :
  ∀ (p : A),
    ∃ (q : A),
      (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 + 1 ∧
        (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 ∈
            cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.1 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 ∧
          (↑q : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 ∈
            cylinder (E := fun (n : ℕ) ↦ ℕ) (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).2.2 (↑p : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1
⊢ False
have choose : ∀ (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),
  False
Tactic: choose F hFn hFx hFy using this
Cleared hypotheses: this
-- 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
⊢ False
have prec : ∀ (n : ℕ), p (n + 1) = F (p n)
Tactic: have prec : ∀ n, p (n + 1) = F (p n) := fun n => by simp only [p, iterate_succ', Function.comp]
-- 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)
n : ℕ
⊢ (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n
have zero : (↑(p 0) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = 0
Tactic: induction n with
    | zero => rfl
    | succ n IH => simp only [prec, hFn, IH]
Cleared hypotheses: n
-- 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)
n : ℕ
zero : (↑(p 0) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = 0
⊢ (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n
have succ : ∀ (n : ℕ) (IH : (↑(p n) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n), (↑(p (n + 1)) : ℕ × (ℕ → ℕ) × (ℕ → ℕ)).1 = n + 1
Tactic: induction n with
    | zero => rfl
    | succ n IH => simp only [prec, hFn, IH]
Cleared hypotheses: n