awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 = ∅
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
have inr : ∀ (h : (s ×ˢ t).Nonempty), MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
Tactic: rcases (s ×ˢ t).eq_empty_or_nonempty with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
have h : ∀ (x : α) (y : β),
  (x, y) ∈ f ⁻¹' s ↔
    Membership.mem (γ := Set (α × β))
      (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)) (x, y)
Tactic: ext1 ⟨x, y⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 : β
⊢ (x, y) ∈ f ⁻¹' s ↔
    Membership.mem (γ := Set (α × β))
      (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y)) (x, y)
have h : f (x, y) ∈ s ↔ ∃ (i : β), f (x, i) ∈ s ∧ y ∈ measurableAtom i
Tactic: simp only [mem_preimage, mem_iUnion, mem_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
have h : (∃ (i : β), f (x, i) ∈ s ∧ y ∈ measurableAtom i) → f (x, y) ∈ s
Tactic: refine ⟨fun h ↦ ⟨y, h, mem_measurableAtom_self y⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
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
⊢ MeasurableSet (f ⁻¹' s)
have this : 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']
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 (f ⁻¹' s)
have rw : MeasurableSet (α := α × β) (⋃ (y : β), SProd.sprod (α := Set α) ((fun (x : α) ↦ f (x, y)) ⁻¹' s) (measurableAtom y))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 f
have change : Measurable (α := α × β) (β := γ) ((fun (p : β × α) ↦ f (p.2, p.1)) ∘ Prod.swap)
Tactic: change Measurable ((fun p ↦ f (p.2, p.1)) ∘ Prod.swap)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 (iUnionLift t f htf T hT ⁻¹' s)
have rw : MeasurableSet (inclusion (s := T) (t := iUnion t) hT ⁻¹' ⋃ (i : ι), inclusion (s := t i) (t := iUnion t) sorry '' f i ⁻¹' s)
Tactic: rw [preimage_iUnionLift]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 (liftCover t f hf htU ⁻¹' s)
have rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), Subtype.val (p := fun (x : α) ↦ x ∈ t i) '' f i ⁻¹' s)
Tactic: rw [preimage_liftCover]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
have inhabit : ∀ (inhabited_h : Inhabited ι), ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
have 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)
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j, hxj
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
⊢ g' i (Subtype.mk (p := fun (x : α) ↦ x ∈ t i) x hxi) = g' j (Subtype.mk (p := fun (x : α) ↦ x ∈ t j) x hxj)
have 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)
Tactic: rcases eq_or_ne i j with rfl | hij
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
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)
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
have ht' : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t 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: have ht' : ∀ (i j) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), g' i ⟨x, hxi⟩ = g' j ⟨x, hxj⟩ := by
    intro i j x hxi hxj
    rcases eq_or_ne i j with rfl | hij
    · rfl
    · exact ht hij ⟨hxi, hxj⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
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)
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t 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)
f : (↑(⋃ (i : ι), t i) : Type u_1) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) ⋯
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
have hfm : Measurable f
Tactic: have hfm : Measurable f := measurable_iUnionLift _ _ t_meas
    (fun i => (hg i).comp measurable_subtype_coe)
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t 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)
f : (↑(⋃ (i : ι), t i) : Type u_1) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) ⋯
hfm : Measurable f
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
have refine : ∀ (i : ι) (x : α) (hx : x ∈ t i),
  (fun (x : α) ↦
        (if hx : Membership.mem (γ := Set α) (⋃ (i : ι), t i) x then
            f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x hx)
          else g default x :
          β))
      x =
    g i x
Tactic: refine ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
      hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t 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)
f : (↑(⋃ (i : ι), t i) : Type u_1) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) ⋯
hfm : Measurable f
i : ι
x : α
hx : x ∈ t i
⊢ (fun (x : α) ↦
        (if hx : Membership.mem (γ := Set α) (⋃ (i : ι), t i) x then
            f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x hx)
          else g default x :
          β))
      x =
    g i x
have simp : f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x sorry) = g i x
Tactic: simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t 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)
f : (↑(⋃ (i : ι), t i) : Type u_1) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) ⋯
hfm : Measurable f
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
have refine : ∀ (i : ι) (x : α) (hx : x ∈ t i),
  (fun (x : α) ↦
        (if hx : Membership.mem (γ := Set α) (⋃ (i : ι), t i) x then
            f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x hx)
          else g default x :
          β))
      x =
    g i x
Tactic: classical
    refine ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
      hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
    simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
    exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
ht' :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t 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)
f : (↑(⋃ (i : ι), t i) : Type u_1) → β := iUnionLift t g' ht' (⋃ (i : ι), t i) ⋯
hfm : Measurable f
refine :
  ∀ (i : ι) (x : α) (hx : x ∈ t i),
    (fun (x : α) ↦
          (if hx : Membership.mem (γ := Set α) (⋃ (i : ι), t i) x then
              f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x hx)
            else g default x :
            β))
        x =
      g i x
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)
have refine₁ : ∀ (i : ι) (x : α) (hx : x ∈ t i),
  f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x sorry) = g i x
Tactic: classical
    refine ⟨fun x => if hx : x ∈ ⋃ i, t i then f ⟨x, hx⟩ else g default x,
      hfm.dite ((hg default).comp measurable_subtype_coe) (.iUnion t_meas), fun i x hx => ?_⟩
    simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
    exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ Measurable g ↔ ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a
have simp_rw : MeasurableSpace.comap g (MeasurableSpace.pi (X := X)) ≤ inst ↔
  ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
Tactic: simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
simp_rw :
  MeasurableSpace.comap g (MeasurableSpace.pi (X := X)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
⊢ Measurable g ↔ ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a
have simp_rw₁ : MeasurableSpace.comap g (⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b a) (inst_1 a)) ≤ inst ↔
  ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
Tactic: simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
simp_rw :
  MeasurableSpace.comap g (MeasurableSpace.pi (X := X)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
simp_rw₁ :
  MeasurableSpace.comap g (⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b a) (inst_1 a)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
⊢ Measurable g ↔ ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a
have simp_rw₂ : ⨆ (i : δ), MeasurableSpace.comap g (MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b i) (inst_1 i)) ≤ inst ↔
  ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
Tactic: simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
simp_rw :
  MeasurableSpace.comap g (MeasurableSpace.pi (X := X)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
simp_rw₁ :
  MeasurableSpace.comap g (⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b a) (inst_1 a)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
simp_rw₂ :
  ⨆ (i : δ), MeasurableSpace.comap g (MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b i) (inst_1 i)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
⊢ Measurable g ↔ ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a
have simp_rw₃ : ⨆ (i : δ), MeasurableSpace.comap ((fun (b : (a : δ) → X a) ↦ b i) ∘ g) (inst_1 i) ≤ inst ↔
  ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
Tactic: simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
simp_rw :
  MeasurableSpace.comap g (MeasurableSpace.pi (X := X)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
simp_rw₁ :
  MeasurableSpace.comap g (⨆ (a : δ), MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b a) (inst_1 a)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
simp_rw₂ :
  ⨆ (i : δ), MeasurableSpace.comap g (MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b i) (inst_1 i)) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
simp_rw₃ :
  ⨆ (i : δ), MeasurableSpace.comap ((fun (b : (a : δ) → X a) ↦ b i) ∘ g) (inst_1 i) ≤ inst ↔
    ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
⊢ Measurable g ↔ ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a
have simp_rw₄ : ⨆ (i : δ), MeasurableSpace.comap (fun (x : α) ↦ g x i) (inst_1 i) ≤ inst ↔
  ∀ (a : δ), MeasurableSpace.comap (fun (x : α) ↦ g x a) (inst_1 a) ≤ inst
Tactic: simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
β : Type u_2
δ : Type u_4
X_1 : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X_1 a)
X : (a : δ) → β → X_1 a
⊢ Eq.{u_2 + 1} (α := MeasurableSpace β)
    (MeasurableSpace.comap (β := (a : δ) → X_1 a) (fun (b : β) (a : δ) ↦ X a b) inferInstance)
    (⨆ (a : δ), MeasurableSpace.comap (X a) inferInstance)
have simp_rw : Eq.{u_2 + 1} (α := MeasurableSpace β)
  (⨆ (i : δ), MeasurableSpace.comap ((fun (b : (a : δ) → X_1 a) ↦ b i) ∘ fun (b : β) (a : δ) ↦ X a b) (inst i))
  (⨆ (a : δ), MeasurableSpace.comap (X a) inferInstance)
Tactic: simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
⊢ Measurable (β := (a : δ) → X a) fun (p : ((i : δ) → X i) × X a) ↦ update (β := X) p.1 a p.2
have rw : ∀ (a_1 : δ), Measurable (β := X a_1) fun (x : ((i : δ) → X i) × X a) ↦ update (β := X) x.1 a x.2 a_1
Tactic: rw [measurable_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
j : δ
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ update (β := X) x.1 a x.2 j
have dsimp : Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦
  if h : j = a then Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 sorry else x.1 j
Tactic: dsimp [update]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
j : δ
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦
    if h : j = a then Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 ⋯ else x.1 j
have pos : ∀ (h : j = a),
  Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
j : δ
pos :
  ∀ (h : j = a),
    Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 ⋯
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦
    if h : j = a then Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 ⋯ else x.1 j
have neg : ∀ (h : ¬j = a), Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ x.1 j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
j : δ
h : j = a
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 ⋯
have pos : Measurable (β := X j) fun (x : ((i : δ) → X i) × X j) ↦ Eq.rec (motive := fun (x : δ) (x_1 : j = x) ↦ X x) x.2 sorry
Tactic: subst h
Cleared hypotheses: a, h