-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem AnalyticSet.measurablySeparable [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α]
    {s t : Set α} (hs : AnalyticSet s) (ht : AnalyticSet t) (h : Disjoint s t) :
    MeasurablySeparable s t

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : AnalyticSet s
ht : AnalyticSet t
h : Disjoint s t
⊢ MeasurablySeparable s t

Tactic:
rw [AnalyticSet] at hs ht

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint ∅ t
⊢ Disjoint t ∅

Tactic:
simp

Result:
no goals

Proof state:
case inr.intro.intro.inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
g : (ℕ → ℕ) → α
g_cont : Continuous g
h : Disjoint (range f) (range g)
⊢ MeasurablySeparable (range f) (range g)

Tactic:
exact measurablySeparable_range_of_disjoint f_cont g_cont h

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
s t : Set α
hs : s = ∅ ∨ ∃ f, Continuous f ∧ range f = s
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint s t
⊢ MeasurablySeparable s t

Tactic:
rcases hs with (rfl | ⟨f, f_cont, rfl⟩)

Result:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint ∅ t
⊢ MeasurablySeparable ∅ t

case inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) t
⊢ MeasurablySeparable (range f) t

Proof state:
case inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) t
⊢ MeasurablySeparable (range f) t

Tactic:
rcases ht with (rfl | ⟨g, g_cont, rfl⟩)

Result:
case inr.intro.intro.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) ∅
⊢ MeasurablySeparable (range f) ∅

case inr.intro.intro.inr.intro.intro
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
g : (ℕ → ℕ) → α
g_cont : Continuous g
h : Disjoint (range f) (range g)
⊢ MeasurablySeparable (range f) (range g)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) ∅
⊢ Disjoint ∅ univ

Tactic:
simp

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
t : Set α
ht : t = ∅ ∨ ∃ f, Continuous f ∧ range f = t
h : Disjoint ∅ t
⊢ MeasurablySeparable ∅ t

Tactic:
refine ⟨∅, Subset.refl _, by simp, MeasurableSet.empty⟩

Result:
no goals

Proof state:
case inr.intro.intro.inl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : T2Space α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
f : (ℕ → ℕ) → α
f_cont : Continuous f
h : Disjoint (range f) ∅
⊢ MeasurablySeparable (range f) ∅

Tactic:
exact ⟨univ, subset_univ _, by simp, MeasurableSet.univ⟩

Result:
no goals