α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ ↑↑μ (⋃ (i : α) (_ : i ∈ s), Iic i) = ↑↑μ univ

α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ DirectedOn ((fun x x_1 => x ⊆ x_1) on fun x => Iic x) s
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ (⨆ (x : α) (_ : x ∈ s), ↑↑μ (Iic x)) = ↑↑μ univ
rw [← measure_biUnion_eq_iSup hsc]
case e_a
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ (⋃ (i : α) (_ : i ∈ s), Iic i) = univ
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ ↑↑μ (⋃ (i : α) (_ : i ∈ s), Iic i) = ↑↑μ univ
congr
case e_a
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hst : ∀ (x : α), ∃ x_1 x_2, x ≤ x_1
⊢ (⋃ (i : α) (_ : i ∈ s), Iic i) = univ
case e_a
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ (⋃ (i : α) (_ : i ∈ s), Iic i) = univ
simp only [← bex_def] at hst
no goals
case e_a
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hst : ∀ (x : α), ∃ x_1 x_2, x ≤ x_1
⊢ (⋃ (i : α) (_ : i ∈ s), Iic i) = univ
exact iUnion₂_eq_univ_iff.2 hst
no goals
α : Type u_1
β : Type ?u.593622
γ : Type ?u.593625
δ : Type ?u.593628
ι : Type ?u.593631
R : Type ?u.593634
R' : Type ?u.593637
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Preorder α
s : Set α
hsc : Set.Countable s
hst : ∀ (x : α), ∃ y, y ∈ s ∧ x ≤ y
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ DirectedOn ((fun x x_1 => x ⊆ x_1) on fun x => Iic x) s
exact directedOn_iff_directed.2 (hdir.directed_val.mono_comp _ fun x y => Iic_subset_Iic.2)