awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
y : β
⊢ Measurable (β := α × β) fun (x : α) ↦ (x, y)

Tactic:
measurable_id.prodMk measurable_const

Premises used: measurable_id, Measurable.prodMk, measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β → γ
hf : Measurable (uncurry f)
x : α
⊢ Measurable (f x)

Tactic:
hf.comp measurable_prodMk_left

Premises used: Measurable.comp, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β → γ
hf : Measurable (uncurry f)
y : β
⊢ Measurable.{u_1, u_3} (β := γ) fun (x : α) ↦ f x y

Tactic:
hf.comp measurable_prodMk_right

Premises used: Measurable.comp, measurable_prodMk_right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
f : α → β × γ
⊢ Measurable f ↔
    (Measurable.{u_1, u_2} (β := β) fun (a : α) ↦ (f a).1) ∧ Measurable.{u_1, u_3} (β := γ) fun (a : α) ↦ (f a).2

Tactic:
⟨fun hf => ⟨measurable_fst.comp hf, measurable_snd.comp hf⟩, fun h => Measurable.prod h.1 h.2⟩

Premises used: Measurable.comp, And.right, And.left, measurable_snd, And.intro, Iff.intro, Measurable.prod, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
⊢ Measurable (α := α × β) Prod.swap

Tactic:
Measurable.prod measurable_snd measurable_fst

Premises used: measurable_snd, Measurable.prod, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
x : MeasurableSpace γ
f : α × β → γ
⊢ Measurable (f ∘ Prod.swap) ↔ Measurable f

Tactic:
⟨fun hf => hf.comp measurable_swap, fun hf => hf.comp measurable_swap⟩

Premises used: Measurable.comp, measurable_swap, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ MeasurableSet (s ×ˢ t)

Tactic:
MeasurableSet.inter (measurable_fst hs) (measurable_snd ht)

Premises used: Set.Mem, setOf, Set.prod, measurable_snd, measurable_fst, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
rcases :
  ∀ (x : α) (y : β) (hx : (x, y).1 ∈ s) (hy : (x, y).2 ∈ t), MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
rcases h with ⟨⟨x, y⟩, hx, hy⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
⟨fun hst => ?_, fun h => h.1.prod h.2⟩

Premises used: MeasurableSet.prod, And.right, And.left, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
refine : ∀ (hst : MeasurableSet (s ×ˢ t)), MeasurableSet s ∧ MeasurableSet t
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t

Tactic:
refine ⟨fun hst => ?_, fun h => h.1.prod h.2⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
⊢ MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t)

Tactic:
have : MeasurableSet ((fun x => (x, y)) ⁻¹' s ×ˢ t) := measurable_prodMk_right hst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this : MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t)
⊢ MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)

Tactic:
have : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t) := measurable_prodMk_left hst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
x : α
y : β
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ t
hst : MeasurableSet (s ×ˢ t)
this_1 : MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t)
this : MeasurableSet (Prod.mk x ⁻¹' s ×ˢ t)
⊢ MeasurableSet s ∧ MeasurableSet t

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
inl : ∀ (h : s ×ˢ t = ∅), MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
inr : ∀ (h : (s ×ˢ t).Nonempty), MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
rcases (s ×ˢ t).eq_empty_or_nonempty with h | h

Premises used: SProd.sprod, Set.eq_empty_or_nonempty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : s ×ˢ t = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [h, prod_eq_empty_iff.mp h]

Premises used: Iff.mp, Set.prod_eq_empty_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]

Premises used: Set.not_nonempty_iff_eq_empty, measurableSet_prod_of_nonempty, Set.prod_nonempty_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set (α × β)
⊢ MeasurableSet (Prod.swap ⁻¹' s) ↔ MeasurableSet s

Tactic:
⟨fun hs => measurable_swap hs, fun hs => measurable_swap hs⟩

Premises used: measurable_swap, Iff.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : MeasurableSingletonClass α
inst_1 : MeasurableSingletonClass β
⊢ MeasurableSingletonClass (α × β)

Tactic:
⟨fun ⟨a, b⟩ => @singleton_prod_singleton _ _ a b ▸ .prod (.singleton a) (.singleton b)⟩

Premises used: MeasurableSet.singleton, MeasurableSet, Eq.rec, MeasurableSet.prod, Set.singleton_prod_singleton, MeasurableSingletonClass.mk, _private.0.Prod.instMeasurableSingletonClass.match_1, Singleton.singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) fun (x : α) ↦ f (x, y)
h'f : ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)
s : Set γ
hs : MeasurableSet s
h :
  ∀ (x : α) (y : β),
    (x, y) ∈ f ⁻¹' s ↔
      Membership.mem (γ := Set (α × β))
        (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)) (x, y)
⊢ f ⁻¹' s = ⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)

Tactic:
ext1 ⟨x, y⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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 : β
h : f (x, y) ∈ s ↔ ∃ (i : β), f (x, i) ∈ s ∧ y ∈ measurableAtom i
⊢ (x, y) ∈ f ⁻¹' s ↔
    Membership.mem (γ := Set (α × β))
      (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)) (x, y)

Tactic:
simp only [mem_preimage, mem_iUnion, mem_prod]

Premises used: Set.mem_iUnion, Set.mem_prod, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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:
⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩

Premises used: mem_measurableAtom_self, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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 : β
h : (∃ (i : β), f (x, i) ∈ s ∧ y ∈ measurableAtom i) → f (x, y) ∈ s
⊢ f (x, y) ∈ s ↔ ∃ (i : β), f (x, i) ∈ s ∧ y ∈ measurableAtom i

Tactic:
refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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'
h h₁ h₂ h₃ : f (x, y') ∈ s
⊢ f (x, y) ∈ s

Tactic:
rwa [h'f y' y x hy']
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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 : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)

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']
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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 : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)
rw :
  MeasurableSet (α := α × β) (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y))
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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 : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)
⊢ MeasurableSet (α := α × β) (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y))

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

Premises used: MeasurableSet.prod, MeasurableSet.measurableAtom_of_countable, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) 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 : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)
⊢ MeasurableSet (α := α × β) (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y))

Tactic:
exact .iUnion (fun y ↦ (hf y hs).prod (.measurableAtom_of_countable y))
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable α
f : α × β → γ
hf : ∀ (x : α), Measurable.{u_2, u_3} (β := γ) fun (y : β) ↦ f (x, y)
h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)
change : Measurable (α := α × β) (β := γ) ((fun (p : β × α) ↦ f (p.2, p.1)) ∘ Prod.swap)
⊢ Measurable f

Tactic:
change Measurable ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)

Premises used: Measurable, Function.comp, Prod.mk, Prod.swap
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable α
f : α × β → γ
hf : ∀ (x : α), Measurable.{u_2, u_3} (β := γ) fun (y : β) ↦ f (x, y)
h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)
⊢ Measurable (α := α × β) (β := γ) ((fun (p : β × α) ↦ f (p.2, p.1)) ∘ Prod.swap)

Tactic:
(measurable_from_prod_countable_left' hf h'f).comp measurable_swap

Premises used: Measurable.comp, measurable_swap, measurable_from_prod_countable_left'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable α
f : α × β → γ
hf : ∀ (x : α), Measurable.{u_2, u_3} (β := γ) fun (y : β) ↦ f (x, y)
h'f : ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)
⊢ Measurable (α := α × β) (β := γ) ((fun (p : β × α) ↦ f (p.2, p.1)) ∘ Prod.swap)

Tactic:
exact (measurable_from_prod_countable_left' hf h'f).comp measurable_swap

Premises used: Measurable.comp, measurable_swap, measurable_from_prod_countable_left'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable β
inst_1 : MeasurableSingletonClass β
f : α × β → γ
hf : ∀ (y : β), Measurable.{u_1, u_3} (β := γ) fun (x : α) ↦ f (x, y)
⊢ ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)

Tactic:
simp +contextual
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : Countable α
inst_1 : MeasurableSingletonClass α
f : α × β → γ
hf : ∀ (x : α), Measurable.{u_2, u_3} (β := γ) fun (y : β) ↦ f (x, y)
⊢ ∀ (x x' : α) (y : β), x' ∈ measurableAtom x → f (x', y) = f (x, y)

Tactic:
simp +contextual
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
x : MeasurableSpace α
f : ℕ → α → β
p : ℕ → α → Prop
inst : (n : ℕ) → DecidablePred (p n)
hf : ∀ (n : ℕ), Measurable (f n)
hp : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {x : α | p n x}
h : ∀ (x : α), ∃ (n : ℕ), p n x
⊢ Measurable.{u_1, u_2} (β := β) fun (x : α) ↦ f (Nat.find (p := fun (n : ℕ) ↦ p n x) ⋯) x

Tactic:
have : Measurable fun p : α × ℕ => f p.2 p.1 := measurable_from_prod_countable_left fun n => hf n
  this.comp (Measurable.prodMk measurable_id (measurable_find h hp))

Premises used: Measurable.comp, measurable_id, Measurable.prodMk, Nat.find, measurable_from_prod_countable_left, measurable_find
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
t : ι → Set α
f : (i : ι) → (↑(t i) : Type u_1) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
rw :
  MeasurableSet
    (inclusion (s := T) (t := iUnion t) hT ⁻¹' ⋃ (i : ι), inclusion (s := t i) (t := iUnion t) ⋯ '' f i ⁻¹' s)
⊢ MeasurableSet (iUnionLift t f htf T hT ⁻¹' s)

Tactic:
rw [preimage_iUnionLift]

Premises used: Set.preimage_iUnionLift
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
t : ι → Set α
f : (i : ι) → (↑(t i) : Type u_1) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet
    (inclusion (s := T) (t := iUnion t) hT ⁻¹' ⋃ (i : ι), inclusion (s := t i) (t := iUnion t) ⋯ '' f i ⁻¹' s)

Tactic:
.preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)

Premises used: MeasurableSet.preimage, MeasurableSet.image_inclusion, Set.subset_iUnion, MeasurableSet.iUnion, measurable_inclusion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
t : ι → Set α
f : (i : ι) → (↑(t i) : Type u_1) → β
htf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
T : Set α
hT : T ⊆ ⋃ (i : ι), t i
htm : ∀ (i : ι), MeasurableSet (t i)
hfm : ∀ (i : ι), Measurable (f i)
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet
    (inclusion (s := T) (t := iUnion t) hT ⁻¹' ⋃ (i : ι), inclusion (s := t i) (t := iUnion t) ⋯ '' f i ⁻¹' s)

Tactic:
exact .preimage (.iUnion fun i => .image_inclusion _ (htm _) (hfm i hs)) (measurable_inclusion _)
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → (↑(t i) : Type u_1) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
htU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), t i) univ
s : Set β
hs : MeasurableSet s
rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ t i) '' f i ⁻¹' s)
⊢ MeasurableSet (liftCover t f hf htU ⁻¹' s)

Tactic:
rw [preimage_liftCover]

Premises used: Set.preimage_liftCover
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → (↑(t i) : Type u_1) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
htU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), t i) univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ t i) '' f i ⁻¹' s)

Tactic:
.iUnion fun i => .subtype_image (htm i) <| hfm i hs

Premises used: MeasurableSet.subtype_image, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
ι : Sort uι
m : MeasurableSpace α
mβ : MeasurableSpace β
inst : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → (↑(t i) : Type u_1) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = f j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
htU : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), t i) univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ t i) '' f i ⁻¹' s)

Tactic:
exact .iUnion fun i => .subtype_image (htm i) <| hfm i hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst : Countable ι
inst_1 : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun (i j : ι) ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabit : ∀ (inhabited_h : Inhabited ι), ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

Tactic:
inhabit ι
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst : Countable ι
inst_1 : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun (i j : ι) ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → (↑(t i) : Type u_1) → β := fun (i : ι) ↦ g i ∘ Subtype.val (p := fun (x : α) ↦ x ∈ t i)
i j : ι
x : α
hxi : x ∈ t i
hxj : x ∈ t j
inl :
  ∀ (hxj : x ∈ t i),
    g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxj)
inr :
  ∀ (hij : i ≠ j),
    g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
⊢ g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)

Tactic:
rcases eq_or_ne i j with rfl | hij

Premises used: eq_or_ne, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst : Countable ι
inst_1 : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun (i j : ι) ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → (↑(t i) : Type u_1) → β := fun (i : ι) ↦ g i ∘ Subtype.val (p := fun (x : α) ↦ x ∈ t i)
i : ι
x : α
hxi hxj : x ∈ t i
⊢ g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxj)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_6
inst : Countable ι
inst_1 : Nonempty ι
t : ι → Set α
t_meas : ∀ (n : ι), MeasurableSet (t n)
g : ι → α → β
hg : ∀ (n : ι), Measurable (g n)
ht : Pairwise fun (i j : ι) ↦ EqOn (g i) (g j) (t i ∩ t j)
inhabited_h : Inhabited ι
g' : (i : ι) → (↑(t i) : Type u_1) → β := fun (i : ι) ↦ g i ∘ Subtype.val (p := fun (x : α) ↦ x ∈ t i)
i j : ι
x : α
hxi : x ∈ t i
hxj : x ∈ t j
hij : i ≠ j
⊢ g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)

Tactic:
ht hij ⟨hxi, hxj⟩

Premises used: And.intro