case a
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Prod.instMeasurableSpace ≤ generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D)

case a
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D) ≤ Prod.instMeasurableSpace
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Prod.instMeasurableSpace = generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D)
apply le_antisymm
case a.refine'_1.h.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
⊢ MeasurableSet (Prod.fst ⁻¹' s)

case a.refine'_2.h.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
⊢ MeasurableSet (Prod.snd ⁻¹' s)
case a
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ Prod.instMeasurableSpace ≤ generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D)
refine' sup_le _ _ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;>
  rintro _ ⟨s, hs, rfl⟩
case a.refine'_1.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (Prod.fst ⁻¹' s)
case a.refine'_1.h.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
⊢ MeasurableSet (Prod.fst ⁻¹' s)
rcases hD with ⟨t, h1t, h2t⟩
case a.refine'_1.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (⋃ (i : ℕ), s ×ˢ t i)
case a.refine'_1.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (Prod.fst ⁻¹' s)
rw [← prod_univ, ← h2t, prod_iUnion]
case a.refine'_1.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ ∀ (b : ℕ), MeasurableSet (s ×ˢ t b)
case a.refine'_1.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (⋃ (i : ℕ), s ×ˢ t i)
apply MeasurableSet.iUnion
case a.refine'_1.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ MeasurableSet (s ×ˢ t n)
case a.refine'_1.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
⊢ ∀ (b : ℕ), MeasurableSet (s ×ˢ t b)
intro n
case a.refine'_1.h.intro.intro.intro.intro.h.ht
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ s ×ˢ t n ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
case a.refine'_1.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ MeasurableSet (s ×ˢ t n)
apply measurableSet_generateFrom
no goals
case a.refine'_1.h.intro.intro.intro.intro.h.ht
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
s : Set α
hs : s ∈ C
t : ℕ → Set β
h1t : ∀ (n : ℕ), t n ∈ D
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ s ×ˢ t n ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
exact ⟨s, t n, hs, h1t n, rfl⟩
case a.refine'_2.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (Prod.snd ⁻¹' s)
case a.refine'_2.h.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
⊢ MeasurableSet (Prod.snd ⁻¹' s)
rcases hC with ⟨t, h1t, h2t⟩
case a.refine'_2.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (⋃ (i : ℕ), t i ×ˢ s)
case a.refine'_2.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (Prod.snd ⁻¹' s)
rw [← univ_prod, ← h2t, iUnion_prod_const]
case a.refine'_2.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
⊢ ∀ (b : ℕ), MeasurableSet (t b ×ˢ s)
case a.refine'_2.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
⊢ MeasurableSet (⋃ (i : ℕ), t i ×ˢ s)
apply MeasurableSet.iUnion
case a.refine'_2.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ MeasurableSet (t n ×ˢ s)
case a.refine'_2.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
⊢ ∀ (b : ℕ), MeasurableSet (t b ×ˢ s)
rintro n
case a.refine'_2.h.intro.intro.intro.intro.h.ht
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ t n ×ˢ s ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
case a.refine'_2.h.intro.intro.intro.intro.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ MeasurableSet (t n ×ˢ s)
apply measurableSet_generateFrom
no goals
case a.refine'_2.h.intro.intro.intro.intro.h.ht
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : (⋃ (n : ℕ), t n) = univ
n : ℕ
⊢ t n ×ˢ s ∈ image2 (fun x x_1 => x ×ˢ x_1) C D
exact mem_image2_of_mem (h1t n) hs
case a.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ (t : Set (α × β)), t ∈ image2 (fun x x_1 => x ×ˢ x_1) C D → MeasurableSet t
case a
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (image2 (fun x x_1 => x ×ˢ x_1) C D) ≤ Prod.instMeasurableSpace
apply generateFrom_le
case a.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet ((fun x x_1 => x ×ˢ x_1) s t)
case a.h
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ (t : Set (α × β)), t ∈ image2 (fun x x_1 => x ×ˢ x_1) C D → MeasurableSet t
rintro _ ⟨s, t, hs, ht, rfl⟩
case a.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet (s ×ˢ t)
case a.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet ((fun x x_1 => x ×ˢ x_1) s t)
dsimp only
case a.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
case a.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet (s ×ˢ t)
rw [prod_eq]
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet s

α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet t
case a.h.intro.intro.intro.intro
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t)
apply (measurable_fst _).inter (measurable_snd _)
no goals
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet s
exact measurableSet_generateFrom hs
no goals
α✝ : Type ?u.538256
α' : Type ?u.538259
β✝ : Type ?u.538262
β' : Type ?u.538265
γ : Type ?u.538268
E : Type ?u.538271
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace α'
inst✝³ : MeasurableSpace β✝
inst✝² : MeasurableSpace β'
inst✝¹ : MeasurableSpace γ
μ μ' : MeasureTheory.Measure α✝
ν ν' : MeasureTheory.Measure β✝
τ : MeasureTheory.Measure γ
inst✝ : NormedAddCommGroup E
α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
t : Set β
hs : s ∈ C
ht : t ∈ D
⊢ MeasurableSet t
exact measurableSet_generateFrom ht