-- Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
lemma MeasurableEmbedding.prodMap {α β γ δ : Type*} {mα : MeasurableSpace α}
    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β}
    {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
    MeasurableEmbedding (Prod.map g f)

Proof state:
case refine_2.basic
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s✝ s : Set (γ × α)
hs : s ∈ image2 (fun x1 x2 => x1 ×ˢ x2) {s | MeasurableSet s} {t | MeasurableSet t}
⊢ MeasurableSet (Prod.map g f '' s)

Tactic:
obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := hs

Result:
case refine_2.basic.intro.intro.intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
t₁ : Set γ
ht₁ : t₁ ∈ {s | MeasurableSet s}
t₂ : Set α
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet (Prod.map g f '' (fun x1 x2 => x1 ×ˢ x2) t₁ t₂)

Proof state:
case refine_2.basic.intro.intro.intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
t₁ : Set γ
ht₁ : t₁ ∈ {s | MeasurableSet s}
t₂ : Set α
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet (Prod.map g f '' (fun x1 x2 => x1 ×ˢ x2) t₁ t₂)

Tactic:
simp_rw [Prod.map, ← prod_image_image_eq]

Result:
case refine_2.basic.intro.intro.intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
t₁ : Set γ
ht₁ : t₁ ∈ {s | MeasurableSet s}
t₂ : Set α
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet ((g '' t₁) ×ˢ (f '' t₂))

Proof state:
case refine_1
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ Measurable (Prod.map g f)

Tactic:
exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd)

Result:
no goals

Proof state:
case refine_2.basic.intro.intro.intro.intro
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
t₁ : Set γ
ht₁ : t₁ ∈ {s | MeasurableSet s}
t₂ : Set α
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ MeasurableSet ((g '' t₁) ×ˢ (f '' t₂))

Tactic:
exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)

Result:
no goals

Proof state:
case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ ∀ ⦃s : Set (γ × α)⦄, MeasurableSet s → MeasurableSet (Prod.map g f '' s)

Tactic:
intro s hs

Result:
case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.map g f '' s)

Proof state:
case refine_2.iUnion
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f✝ : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f✝
s : Set (γ × α)
f : ℕ → Set (γ × α)
a✝ : Pairwise (Function.onFun Disjoint f)
hfm✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), MeasurableSet (Prod.map g f✝ '' f i)
⊢ MeasurableSet (Prod.map g f✝ '' ⋃ i, f i)

Tactic:
simpa only [image_iUnion] using .iUnion ihf

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ MeasurableEmbedding (Prod.map g f)

Tactic:
refine ⟨hg.injective.prodMap hf.injective, ?_, ?_⟩

Result:
case refine_1
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ Measurable (Prod.map g f)

case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
⊢ ∀ ⦃s : Set (γ × α)⦄, MeasurableSet s → MeasurableSet (Prod.map g f '' s)

Proof state:
case refine_2.compl
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s✝ s : Set (γ × α)
htm✝ : MeasurableSet s
ihs : MeasurableSet (Prod.map g f '' s)
⊢ MeasurableSet (range g ×ˢ range f \ Prod.map g f '' s)

Tactic:
exact .diff (.prod hg.measurableSet_range hf.measurableSet_range) ihs

Result:
no goals

Proof state:
case refine_2.empty
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
⊢ MeasurableSet (Prod.map g f '' ∅)

Tactic:
simp only [Set.image_empty, MeasurableSet.empty]

Result:
no goals

Proof state:
case refine_2.compl
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s✝ s : Set (γ × α)
htm✝ : MeasurableSet s
ihs : MeasurableSet (Prod.map g f '' s)
⊢ MeasurableSet (Prod.map g f '' sᶜ)

Tactic:
rw [← range_diff_image (hg.injective.prodMap hf.injective), range_prod_map]

Result:
case refine_2.compl
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s✝ s : Set (γ × α)
htm✝ : MeasurableSet s
ihs : MeasurableSet (Prod.map g f '' s)
⊢ MeasurableSet (range g ×ˢ range f \ Prod.map g f '' s)

Proof state:
case refine_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
f : α → β
g : γ → δ
hg : MeasurableEmbedding g
hf : MeasurableEmbedding f
s : Set (γ × α)
hs : MeasurableSet s
⊢ MeasurableSet (Prod.map g f '' s)

Tactic:
induction s, hs using induction_on_inter generateFrom_prod.symm isPiSystem_prod with
| empty =>
  simp only [Set.image_empty, MeasurableSet.empty]
| basic s hs =>
  obtain ⟨t₁, ht₁, t₂, ht₂, rfl⟩ := hs
  simp_rw [Prod.map, ← prod_image_image_eq]
  exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)
| compl s _ ihs =>
  rw [← range_diff_image (hg.injective.prodMap hf.injective), range_prod_map]
  exact .diff (.prod hg.measurableSet_range hf.measurableSet_range) ihs
| iUnion f _ _ ihf =>
  simpa only [image_iUnion] using .iUnion ihf

Result:
no goals