case refine'_1
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ ⨆ (i : ι) (_ : i ∈ S), m i

case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ (⨆ (i : ι) (_ : i ∈ S), m i) ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) = ⨆ (i : ι) (_ : i ∈ S), m i
refine' le_antisymm _ _
case refine'_1
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}
case refine'_1
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ ⨆ (i : ι) (_ : i ∈ S), m i
rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]
no goals
case refine'_1
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}
exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ (⨆ (i : ι) (_ : i ∈ S), m i) ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
refine' iSup₂_le fun i hi => _
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ generateFrom {s | MeasurableSet s} ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
rw [← @generateFrom_measurableSet α (m i)]
no goals
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ generateFrom {s | MeasurableSet s} ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)