α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
⊢ MeasurableEmbedding fun x => (g x.fst, f x.snd)
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableEmbedding fun x => (g x.fst, f x.snd)
have h_inj : Function.Injective fun x : γ × α => (g x.fst, f x.snd) := by
  intro x y hxy
  rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
  simp only [Prod.mk.inj_iff] at hxy⊢
  exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩
case refine'_1
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
⊢ Measurable fun x => (g x.fst, f x.snd)

case refine'_2
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
⊢ ∀ ⦃s : Set (γ × α)⦄, MeasurableSet s → MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
⊢ MeasurableEmbedding fun x => (g x.fst, f x.snd)
refine' ⟨h_inj, _, _⟩
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
x y : γ × α
hxy : (fun x => (g x.fst, f x.snd)) x = (fun x => (g x.fst, f x.snd)) y
⊢ x = y
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ Injective fun x => (g x.fst, f x.snd)
intro x y hxy
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
x y : γ × α
hxy : (fun x => (g x.fst, f x.snd)) x = (fun x => (g x.fst, f x.snd)) y
⊢ (x.fst, x.snd) = (y.fst, y.snd)
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
x y : γ × α
hxy : (fun x => (g x.fst, f x.snd)) x = (fun x => (g x.fst, f x.snd)) y
⊢ x = y
rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
x y : γ × α
hxy : g x.fst = g y.fst ∧ f x.snd = f y.snd
⊢ x.fst = y.fst ∧ x.snd = y.snd
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
x y : γ × α
hxy : (fun x => (g x.fst, f x.snd)) x = (fun x => (g x.fst, f x.snd)) y
⊢ (x.fst, x.snd) = (y.fst, y.snd)
simp only [Prod.mk.inj_iff] at hxy⊢
no goals
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
x y : γ × α
hxy : g x.fst = g y.fst ∧ f x.snd = f y.snd
⊢ x.fst = y.fst ∧ x.snd = y.snd
exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩
no goals
case refine'_1
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
⊢ Measurable fun x => (g x.fst, f x.snd)
exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd)
case refine'_2.refine'_1
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) ∅

case refine'_2.refine'_2
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ ∀ (t : Set (γ × α)),
    t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t} →
      (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) t

case refine'_2.refine'_3
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ ∀ (t : Set (γ × α)),
    MeasurableSet t →
      (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) t →
        (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) (tᶜ)

case refine'_2.refine'_4
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ ∀ (f_1 : ℕ → Set (γ × α)),
    Pairwise (Disjoint on f_1) →
      (∀ (i : ℕ), MeasurableSet (f_1 i)) →
        (∀ (i : ℕ), (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) (f_1 i)) →
          (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) (⋃ (i : ℕ), f_1 i)
case refine'_2
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
⊢ ∀ ⦃s : Set (γ × α)⦄, MeasurableSet s → MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)
refine' fun s hs =>
  @MeasurableSpace.induction_on_inter _
    (fun s => MeasurableSet ((fun x : γ × α => (g x.fst, f x.snd)) '' s)) _ _
    generateFrom_prod.symm isPiSystem_prod _ _ _ _ _ hs
no goals
case refine'_2.refine'_1
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) ∅
simp only [Set.image_empty, MeasurableSet.empty]
case refine'_2.refine'_2.intro.intro.intro.intro
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t₁ : Set γ
t₂ : Set α
ht₁ : t₁ ∈ {s | MeasurableSet s}
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet ((fun x => (g x.fst, f x.snd)) '' (fun x x_1 => x ×ˢ x_1) t₁ t₂)
case refine'_2.refine'_2
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ ∀ (t : Set (γ × α)),
    t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t} →
      (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) t
rintro t ⟨t₁, t₂, ht₁, ht₂, rfl⟩
case refine'_2.refine'_2.intro.intro.intro.intro
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t₁ : Set γ
t₂ : Set α
ht₁ : t₁ ∈ {s | MeasurableSet s}
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet ((g '' t₁) ×ˢ (f '' t₂))
case refine'_2.refine'_2.intro.intro.intro.intro
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t₁ : Set γ
t₂ : Set α
ht₁ : t₁ ∈ {s | MeasurableSet s}
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet ((fun x => (g x.fst, f x.snd)) '' (fun x x_1 => x ×ˢ x_1) t₁ t₂)
rw [← Set.prod_image_image_eq]
no goals
case refine'_2.refine'_2.intro.intro.intro.intro
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t₁ : Set γ
t₂ : Set α
ht₁ : t₁ ∈ {s | MeasurableSet s}
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet ((g '' t₁) ×ˢ (f '' t₂))
exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)
case refine'_2.refine'_3
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t : Set (γ × α)
a✝ : MeasurableSet t
ht_m : MeasurableSet ((fun x => (g x.fst, f x.snd)) '' t)
⊢ MeasurableSet ((fun x => (g x.fst, f x.snd)) '' tᶜ)
case refine'_2.refine'_3
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ ∀ (t : Set (γ × α)),
    MeasurableSet t →
      (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) t →
        (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) (tᶜ)
intro t _ ht_m
case refine'_2.refine'_3
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t : Set (γ × α)
a✝ : MeasurableSet t
ht_m : MeasurableSet ((fun x => (g x.fst, f x.snd)) '' t)
⊢ MeasurableSet (range g ×ˢ range f \ (fun x => (g x.fst, f x.snd)) '' t)
case refine'_2.refine'_3
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t : Set (γ × α)
a✝ : MeasurableSet t
ht_m : MeasurableSet ((fun x => (g x.fst, f x.snd)) '' t)
⊢ MeasurableSet ((fun x => (g x.fst, f x.snd)) '' tᶜ)
rw [← Set.range_diff_image h_inj, ← Set.prod_range_range_eq]
no goals
case refine'_2.refine'_3
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
t : Set (γ × α)
a✝ : MeasurableSet t
ht_m : MeasurableSet ((fun x => (g x.fst, f x.snd)) '' t)
⊢ MeasurableSet (range g ×ˢ range f \ (fun x => (g x.fst, f x.snd)) '' t)
exact
  MeasurableSet.diff (MeasurableSet.prod hg.measurableSet_range hf.measurableSet_range) ht_m
case refine'_2.refine'_4
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g✝ : γ → δ
hg✝ : MeasurableEmbedding g✝
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g✝ x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
g : ℕ → Set (γ × α)
a✝¹ : Pairwise (Disjoint on g)
a✝ : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), (fun s => MeasurableSet ((fun x => (g✝ x.fst, f x.snd)) '' s)) (g i)
⊢ MeasurableSet ((fun x => (g✝ x.fst, f x.snd)) '' ⋃ (i : ℕ), g i)
case refine'_2.refine'_4
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
⊢ ∀ (f_1 : ℕ → Set (γ × α)),
    Pairwise (Disjoint on f_1) →
      (∀ (i : ℕ), MeasurableSet (f_1 i)) →
        (∀ (i : ℕ), (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) (f_1 i)) →
          (fun s => MeasurableSet ((fun x => (g x.fst, f x.snd)) '' s)) (⋃ (i : ℕ), f_1 i)
intro g _ _ hg
case refine'_2.refine'_4
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g✝ : γ → δ
hg✝ : MeasurableEmbedding g✝
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g✝ x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
g : ℕ → Set (γ × α)
a✝¹ : Pairwise (Disjoint on g)
a✝ : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), (fun s => MeasurableSet ((fun x => (g✝ x.fst, f x.snd)) '' s)) (g i)
⊢ MeasurableSet (⋃ (i : ℕ), (fun x => (g✝ x.fst, f x.snd)) '' g i)
case refine'_2.refine'_4
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g✝ : γ → δ
hg✝ : MeasurableEmbedding g✝
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g✝ x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
g : ℕ → Set (γ × α)
a✝¹ : Pairwise (Disjoint on g)
a✝ : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), (fun s => MeasurableSet ((fun x => (g✝ x.fst, f x.snd)) '' s)) (g i)
⊢ MeasurableSet ((fun x => (g✝ x.fst, f x.snd)) '' ⋃ (i : ℕ), g i)
simp_rw [Set.image_iUnion]
no goals
case refine'_2.refine'_4
α✝ : Type ?u.3071758
α' : Type ?u.3071761
β✝ : Type ?u.3071764
β' : Type ?u.3071767
γ✝ : Type ?u.3071770
E : Type ?u.3071773
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
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g✝ : γ → δ
hg✝ : MeasurableEmbedding g✝
hf : MeasurableEmbedding f
h_inj : Injective fun x => (g✝ x.fst, f x.snd)
s : Set (γ × α)
hs : MeasurableSet s
g : ℕ → Set (γ × α)
a✝¹ : Pairwise (Disjoint on g)
a✝ : ∀ (i : ℕ), MeasurableSet (g i)
hg : ∀ (i : ℕ), (fun s => MeasurableSet ((fun x => (g✝ x.fst, f x.snd)) '' s)) (g i)
⊢ MeasurableSet (⋃ (i : ℕ), (fun x => (g✝ x.fst, f x.snd)) '' g i)
exact MeasurableSet.iUnion hg