-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_from_prod_countable' [Countable β]
    {_ : MeasurableSpace γ} {f : α × β → γ} (hf : ∀ y, Measurable fun x => f (x, y))
    (h'f : ∀ y y' x, y' ∈ measurableAtom y → f (x, y') = f (x, y)) :
    Measurable f := fun s hs => by
  have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
have : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ (measurableAtom y : Set β) := by
  ext1 ⟨x, y⟩
  simp only [mem_preimage, mem_iUnion, mem_prod]
  refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
  rintro ⟨y', hy's, hy'⟩
  rwa [h'f y' y x hy']

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (f ⁻¹' s)

Proof state:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ f (x, y) ∈ s ↔ ∃ i, f (x, i) ∈ s ∧ y ∈ measurableAtom i

Tactic:
refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (∃ i, f (x, i) ∈ s ∧ y ∈ measurableAtom i) → f (x, y) ∈ s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rw [this]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
this : f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y
⊢ MeasurableSet (⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y)

Tactic:
exact .iUnion (fun y ↦ (hf y hs).prod (.measurableAtom_of_countable y))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
⊢ f ⁻¹' s = ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y

Tactic:
ext1 ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y

Proof state:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (x, y) ∈ f ⁻¹' s ↔ (x, y) ∈ ⋃ y, ((fun x => f (x, y)) ⁻¹' s) ×ˢ measurableAtom y

Tactic:
simp only [mem_preimage, mem_iUnion, mem_prod]

Result:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ f (x, y) ∈ s ↔ ∃ i, f (x, i) ∈ s ∧ y ∈ measurableAtom i

Proof state:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y : β
⊢ (∃ i, f (x, i) ∈ s ∧ y ∈ measurableAtom i) → f (x, y) ∈ s

Tactic:
rintro ⟨y', hy's, hy'⟩

Result:
case h.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y y' : β
hy's : f (x, y') ∈ s
hy' : y ∈ measurableAtom y'
⊢ f (x, y) ∈ s

Proof state:
case h.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
x : α
y y' : β
hy's : f (x, y') ∈ s
hy' : y ∈ measurableAtom y'
⊢ f (x, y) ∈ s

Tactic:
rwa [h'f y' y x hy']

Result:
no goals