case intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ MeasurableSpace.pi = generateFrom (Set.pi univ '' Set.pi univ C)
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
⊢ MeasurableSpace.pi = generateFrom (Set.pi univ '' Set.pi univ C)
cases nonempty_encodable ι
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ MeasurableSpace.pi ≤ generateFrom (Set.pi univ '' Set.pi univ C)

case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ generateFrom (Set.pi univ '' Set.pi univ C) ≤ MeasurableSpace.pi
case intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ MeasurableSpace.pi = generateFrom (Set.pi univ '' Set.pi univ C)
apply le_antisymm
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ MeasurableSpace.pi ≤ generateFrom (Set.pi univ '' Set.pi univ C)
refine' iSup_le _
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (i : ι),
    MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
intro i
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ generateFrom ((preimage fun b => b i) '' C i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ MeasurableSpace.comap (fun b => b i) ((fun i => generateFrom (C i)) i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
rw [comap_generateFrom]
case intro.a.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ (t : Set ((a : ι) → (fun i => α i) a)), t ∈ (preimage fun b => b i) '' C i → MeasurableSet t
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ generateFrom ((preimage fun b => b i) '' C i) ≤ generateFrom (Set.pi univ '' Set.pi univ C)
apply generateFrom_le
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
case intro.a.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
⊢ ∀ (t : Set ((a : ι) → (fun i => α i) a)), t ∈ (preimage fun b => b i) '' C i → MeasurableSet t
rintro _ ⟨s, hs, rfl⟩
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
dsimp
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
choose t h1t h2t using hC
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i s))
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
⊢ MeasurableSet ((fun b => b i) ⁻¹' s)
simp_rw [eval_preimage, ← h2t]
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i (⋃ (x : ℕ), s)))
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i s))
rw [← @iUnion_const _ ℕ _ s]
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ MeasurableSet (⋃ (x : ι → ℕ), Set.pi univ fun i_1 => update (fun i' => t i' (x i_1)) i s i_1)
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ MeasurableSet (Set.pi univ (update (fun i => ⋃ (n : ℕ), t i n) i (⋃ (x : ℕ), s)))
rw [this, ← iUnion_univ_pi]
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ ∀ (b : ι → ℕ), MeasurableSet (Set.pi univ fun i_1 => update (fun i' => t i' (b i_1)) i s i_1)
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ MeasurableSet (⋃ (x : ι → ℕ), Set.pi univ fun i_1 => update (fun i' => t i' (x i_1)) i s i_1)
apply MeasurableSet.iUnion
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ MeasurableSet (Set.pi univ fun i_1 => update (fun i' => t i' (n i_1)) i s i_1)
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
⊢ ∀ (b : ι → ℕ), MeasurableSet (Set.pi univ fun i_1 => update (fun i' => t i' (b i_1)) i s i_1)
intro n
case intro.a.h.intro.intro.h.ht
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ (Set.pi univ fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) ∈ Set.pi univ '' Set.pi univ C
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ MeasurableSet (Set.pi univ fun i_1 => update (fun i' => t i' (n i_1)) i s i_1)
apply measurableSet_generateFrom
case intro.a.h.intro.intro.h.ht.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ (fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) ∈ Set.pi univ C
case intro.a.h.intro.intro.h.ht
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ (Set.pi univ fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) ∈ Set.pi univ '' Set.pi univ C
apply mem_image_of_mem
case intro.a.h.intro.intro.h.ht.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ (fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) j ∈ C j
case intro.a.h.intro.intro.h.ht.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
⊢ (fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) ∈ Set.pi univ C
intro j _
case intro.a.h.intro.intro.h.ht.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
case intro.a.h.intro.intro.h.ht.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ (fun i_1 => update (fun i' => t i' (n i_1)) i s i_1) j ∈ C j
dsimp only
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j

case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
case intro.a.h.intro.intro.h.ht.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
by_cases h : j = i
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
n : ι → ℕ
j : ι
a✝ : j ∈ univ
s : Set ((fun i => α i) j)
hs : s ∈ C j
this :
  Set.pi univ (update (fun i' => iUnion (t i')) j (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j_1 : ℕ), update (fun i' => t i' j_1) j s k
⊢ update (fun i' => t i' (n j)) j s j ∈ C j

case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j

case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
subst h
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
n : ι → ℕ
j : ι
a✝ : j ∈ univ
s : Set ((fun i => α i) j)
hs : s ∈ C j
this :
  Set.pi univ (update (fun i' => iUnion (t i')) j (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j_1 : ℕ), update (fun i' => t i' j_1) j s k
⊢ update (fun i' => t i' (n j)) j s j ∈ C j

case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
rwa [update_same]
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ t j (n j) ∈ C j
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ update (fun i' => t i' (n j)) i s j ∈ C j
rw [update_noteq h]
no goals
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
this :
  Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
n : ι → ℕ
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ t j (n j) ∈ C j
apply h1t
case h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) ↔
    x✝ ∈ Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
⊢ Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) =
    Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
ext
case h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i_1
case h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
⊢ x✝ ∈ Set.pi univ (update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s)) ↔
    x✝ ∈ Set.pi univ fun k => ⋃ (j : ℕ), update (fun i' => t i' j) i s k
simp_rw [mem_univ_pi]
case h.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι),
    x✝ a ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) a ↔ x✝ a ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s a
case h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
⊢ (∀ (i_1 : ι), x✝ i_1 ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i_1) ↔
    ∀ (i_1 : ι), x✝ i_1 ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i_1
apply forall_congr'
case h.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
case h.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
⊢ ∀ (a : ι),
    x✝ a ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) a ↔ x✝ a ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s a
intro i'
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
h : i' = i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'

case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
h : ¬i' = i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
case h.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
by_cases i' = i
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
s : Set ((fun i => α i) i')
hs : s ∈ C i'
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i' (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i' s i'
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
h : i' = i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
subst h
no goals
case pos
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
s : Set ((fun i => α i) i')
hs : s ∈ C i'
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i' (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i' s i'
simp
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
h : i' ≠ i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
h : ¬i' = i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
rw [← Ne.def] at h
no goals
case neg
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
val✝ : Encodable ι
i : ι
s : Set ((fun i => α i) i)
hs : s ∈ C i
t : (i : ι) → ℕ → Set (α i)
h1t : ∀ (i : ι) (n : ℕ), t i n ∈ C i
h2t : ∀ (i : ι), (⋃ (n : ℕ), t i n) = univ
x✝ : (i : ι) → α i
i' : ι
h : i' ≠ i
⊢ x✝ i' ∈ update (fun i' => iUnion (t i')) i (⋃ (x : ℕ), s) i' ↔ x✝ i' ∈ ⋃ (j : ℕ), update (fun i' => t i' j) i s i'
simp [h]
case intro.a.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (t : Set ((i : ι) → α i)), t ∈ Set.pi univ '' Set.pi univ C → MeasurableSet t
case intro.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ generateFrom (Set.pi univ '' Set.pi univ C) ≤ MeasurableSpace.pi
apply generateFrom_le
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ MeasurableSet (Set.pi univ s)
case intro.a.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
⊢ ∀ (t : Set ((i : ι) → α i)), t ∈ Set.pi univ '' Set.pi univ C → MeasurableSet t
rintro _ ⟨s, hs, rfl⟩
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ MeasurableSet (⋂ (i : ι), eval i ⁻¹' s i)
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ MeasurableSet (Set.pi univ s)
rw [univ_pi_eq_iInter]
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)
case intro.a.h.intro.intro
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ MeasurableSet (⋂ (i : ι), eval i ⁻¹' s i)
apply MeasurableSet.iInter
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
i : ι
⊢ MeasurableSet (eval i ⁻¹' s i)
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
⊢ ∀ (b : ι), MeasurableSet (eval b ⁻¹' s b)
intro i
case intro.a.h.intro.intro.h.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
i : ι
⊢ MeasurableSet (s i)
case intro.a.h.intro.intro.h
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
i : ι
⊢ MeasurableSet (eval i ⁻¹' s i)
apply @measurable_pi_apply _ _ (fun i => generateFrom (C i))
no goals
case intro.a.h.intro.intro.h.a
ι : Type u_2
ι' : Type ?u.642179
α : ι → Type u_1
inst✝¹ : Finite ι
inst✝ : Finite ι'
C : (i : ι) → Set (Set (α i))
hC : ∀ (i : ι), IsCountablySpanning (C i)
val✝ : Encodable ι
s : (i : ι) → Set (α i)
hs : s ∈ Set.pi univ C
i : ι
⊢ MeasurableSet (s i)
exact measurableSet_generateFrom (hs i (mem_univ i))