α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 (⋃ (n : ι), s n) (⋃ (m : ι), t m)
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
h : ∀ (m n : ι), MeasurablySeparable (s m) (t n)
⊢ MeasurablySeparable (⋃ (n : ι), s n) (⋃ (m : ι), t m)
choose u hsu htu hu using h
case refine'_1
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 : ι), s n) ⊆ ⋃ (m : ι), ⋂ (n : ι), u m n

case refine'_2
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 (⋃ (m : ι), t m) (⋃ (m : ι), ⋂ (n : ι), u m n)

case refine'_3
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 (⋃ (m : ι), ⋂ (n : ι), u m n)
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 (⋃ (n : ι), s n) (⋃ (m : ι), t m)
refine' ⟨⋃ m, ⋂ n, u m n, _, _, _⟩
case refine'_1
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
m : ι
⊢ s m ⊆ ⋂ (n : ι), u m n
case refine'_1
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 : ι), s n) ⊆ ⋃ (m : ι), ⋂ (n : ι), u m n
refine' iUnion_subset fun m => subset_iUnion_of_subset m _
no goals
case refine'_1
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
m : ι
⊢ s m ⊆ ⋂ (n : ι), u m n
exact subset_iInter fun n => hsu m n
case refine'_2
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
⊢ ∀ (i i_1 : ι), Disjoint (t i) (⋂ (n : ι), u i_1 n)
case refine'_2
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 (⋃ (m : ι), t m) (⋃ (m : ι), ⋂ (n : ι), u m n)
simp_rw [disjoint_iUnion_left, disjoint_iUnion_right]
case refine'_2
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
case refine'_2
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
⊢ ∀ (i i_1 : ι), Disjoint (t i) (⋂ (n : ι), u i_1 n)
intro n m
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 : ι
⊢ (⋂ (n : ι), u m n) ≤ u m n
case refine'_2
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
apply Disjoint.mono_right _ (htu m n)
no goals
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 : ι
⊢ (⋂ (n : ι), u m n) ≤ u m n
apply iInter_subset
case refine'_3
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
m : ι
⊢ MeasurableSet (⋂ (n : ι), u m n)
case refine'_3
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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 (⋃ (m : ι), ⋂ (n : ι), u m n)
refine' MeasurableSet.iUnion fun m => _
no goals
case refine'_3
α✝ : Type ?u.67309
inst✝² : TopologicalSpace α✝
ι : Type u_1
inst✝¹ : Countable ι
α : Type u_2
inst✝ : MeasurableSpace α
s t : ι → Set α
u : ι → ι → 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)
m : ι
⊢ MeasurableSet (⋂ (n : ι), u m n)
exact MeasurableSet.iInter fun n => hu m n