case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ pt), ft x)
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
t : Set α
ht : t ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S
⊢ MeasurableSet t
rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ MeasurableSet (ft i)
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ pt), ft x)
refine' pt.measurableSet_biInter fun i hi => _
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
h_le : m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
⊢ MeasurableSet (ft i)

case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ MeasurableSet (ft i)
suffices h_le : m i ≤ ⨆ i ∈ S, m i
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
h_le : m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
⊢ MeasurableSet (ft i)

case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
exact h_le (ft i) (ht_m i hi)
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
have hi' : i ∈ S := hpt hi
no goals
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
exact le_iSup₂ (f := fun i (_ : i ∈ S) => m i) i hi'