awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ht hij ⟨hxi, hxj⟩

Premises used: And.intro
-- 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),
    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⟩
-- 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)
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) ⋯
⊢ Measurable f

Tactic:
have hfm : Measurable f := measurable_iUnionLift _ _ t_meas
    (fun i => (hg i).comp measurable_subtype_coe)
-- 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)
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)

Tactic:
⟨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 => ?_⟩

Premises used: measurable_subtype_coe, Inhabited.default, Measurable.comp, Membership.mem, dite, Subtype.mk, And.intro, Exists.intro, MeasurableSet.iUnion, Measurable.dite, Set.iUnion
-- 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)
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)

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 => ?_⟩
-- 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)
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
simp : f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x ⋯) = g i x
⊢ (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:
simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]

Premises used: Iff.mpr, Set.mem_iUnion, dif_pos, Exists.intro
-- 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)
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
⊢ f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x ⋯) = g i x

Tactic:
iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx

Premises used: Iff.mpr, Set.iUnionLift_of_mem, Set.mem_iUnion, Subtype.mk, Exists.intro
-- 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)
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
⊢ f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x ⋯) = g i x

Tactic:
exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx

Premises used: Iff.mpr, Set.iUnionLift_of_mem, Set.mem_iUnion, Subtype.mk, Exists.intro
-- 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)
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
refine₁ :
  ∀ (i : ι) (x : α) (hx : x ∈ t i),
    f (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (⋃ (i : ι), t i) x) x ⋯) = g i x
⊢ ∃ (f : α → β), Measurable f ∧ ∀ (n : ι), EqOn f (g n) (t n)

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
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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
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
⊢ Measurable g ↔ ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a

Tactic:
simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup,
    MeasurableSpace.comap_comp, Function.comp_def, iSup_le_iff]

Premises used: MeasurableSpace.comap_comp, measurable_iff_comap_le, MeasurableSpace.comap_iSup, Function.comp_def, MeasurableSpace.pi, iSup_le_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
⊢ Measurable (β := X a) fun (f : (a : δ) → X a) ↦ f a

Tactic:
measurable_pi_iff.1 measurable_id a

Premises used: measurable_pi_iff, measurable_id, Iff.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤
    MeasurableSpace.comap (β := (c : δ) → X c) (fun (b : β) (c : δ) ↦ g c b)
      (MeasurableSpace.comap (fun (b : (a : δ) → X a) ↦ b a) (inst a))

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
g : (a : δ) → β → X a
a : δ
⊢ MeasurableSpace.comap (g a) inferInstance ≤
    MeasurableSpace.comap (β := (c : δ) → X c) (fun (b : β) (c : δ) ↦ g c b) (pi (X := X))

Tactic:
simpa only [pi, comap_iSup] using le_iSup_of_le a <| by measurability

Premises used: MeasurableSpace.comap_iSup, MeasurableSpace.pi, le_iSup_of_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
a : δ
g : α → (a : δ) → X a
hg : Measurable g
⊢ Measurable.{u_1, u_6} (β := X a) fun (x : α) ↦ g x a

Tactic:
(measurable_pi_apply a).comp hg

Premises used: Measurable.comp, measurable_pi_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
f : α → (a : δ) → X a
hf : ∀ (a : δ), Measurable.{u_1, u_6} (β := X a) fun (c : α) ↦ f c a
⊢ Measurable f

Tactic:
measurable_pi_iff.mpr hf

Premises used: Iff.mpr, measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
β : Type u_2
δ : Type u_4
X_1 : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X_1 a)
X : (a : δ) → β → X_1 a
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)
⊢ Eq.{u_2 + 1} (α := MeasurableSpace β)
    (MeasurableSpace.comap (β := (a : δ) → X_1 a) (fun (b : β) (a : δ) ↦ X a b) inferInstance)
    (⨆ (a : δ), MeasurableSpace.comap (X a) inferInstance)

Tactic:
simp_rw [MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp]

Premises used: MeasurableSpace.comap_comp, MeasurableSpace.comap_iSup, MeasurableSpace.pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 β)
    (⨆ (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:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
rw : ∀ (a_1 : δ), Measurable (β := X a_1) fun (x : ((i : δ) → X i) × X a) ↦ update (β := X) x.1 a x.2 a_1
⊢ Measurable (β := (a : δ) → X a) fun (p : ((i : δ) → X i) × X a) ↦ update (β := X) p.1 a p.2

Tactic:
rw [measurable_pi_iff]

Premises used: measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
j : δ
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 ⋯ else x.1 j
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ update (β := X) x.1 a x.2 j

Tactic:
dsimp [update]

Premises used: Function.update
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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 ⋯
neg : ∀ (h : ¬j = a), Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ x.1 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

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
j : δ
h : j = a
pos : Measurable (β := X j) fun (x : ((i : δ) → X i) × X j) ↦ Eq.rec (motive := fun (x : δ) (x_1 : j = x) ↦ X x) x.2 ⋯
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X a) ↦ Eq.rec (motive := fun (x : δ) (x_1 : a = x) ↦ X x) x.2 ⋯

Tactic:
subst h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
j : δ
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X j) ↦ x.2

Tactic:
measurable_snd

Premises used: measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
j : δ
⊢ Measurable (β := X j) fun (x : ((i : δ) → X i) × X j) ↦ x.2

Tactic:
exact measurable_snd

Premises used: measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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) ↦ x.1 j

Tactic:
measurable_pi_iff.1 measurable_fst _

Premises used: measurable_pi_iff, Iff.mp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
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) ↦ x.1 j

Tactic:
exact measurable_pi_iff.1 measurable_fst _

Premises used: measurable_pi_iff, Iff.mp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : Unique δ
simp_rw : Measurable (β := X default) fun (x : X default) ↦ x
⊢ Measurable (α := X default) (uniqueElim (α := X))

Tactic:
simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]

Premises used: measurable_pi_iff, Unique.forall_iff, uniqueElim_default
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : Unique δ
⊢ Measurable (β := X default) fun (x : X default) ↦ x

Tactic:
measurable_id

Premises used: measurable_id
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : Unique δ
⊢ Measurable (β := X default) fun (x : X default) ↦ x

Tactic:
exact measurable_id

Premises used: measurable_id
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
simp :
  ∀ (a : δ),
    Measurable (β := X a) fun (x : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦
      if hi : a ∈ s then x.2 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) a hi) else x.1 a
⊢ Measurable (β := (i : δ) → X i) fun (p : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦ updateFinset (π := X) p.1 s p.2

Tactic:
simp only [updateFinset, measurable_pi_iff]

Premises used: measurable_pi_iff, Function.updateFinset
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
i : δ
pos :
  ∀ (h : i ∈ s),
    Measurable (β := X i) fun (x : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦
      if hi : i ∈ s then x.2 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi) else x.1 i
neg :
  ∀ (h : i ∉ s),
    Measurable (β := X i) fun (x : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦
      if hi : i ∈ s then x.2 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi) else x.1 i
⊢ Measurable (β := X i) fun (x : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦
    if hi : i ∈ s then x.2 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi) else x.1 i

Tactic:
by_cases h : i ∈ s
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
i : δ
h : i ∈ s
⊢ Measurable (β := X i) fun (x : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦
    if hi : i ∈ s then x.2 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi) else x.1 i

Tactic:
simp [h, Measurable.eval, measurable_fst, measurable_snd]

Premises used: measurable_snd, Measurable.eval, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
i : δ
h : i ∉ s
⊢ Measurable (β := X i) fun (x : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦
    if hi : i ∈ s then x.2 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi) else x.1 i

Tactic:
simp [h, Measurable.eval, measurable_fst, measurable_snd]

Premises used: measurable_snd, Measurable.eval, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
x : (i : δ) → X i
⊢ Measurable (updateFinset (π := X) x s)

Tactic:
measurable_updateFinset'.comp measurable_prodMk_left

Premises used: Function.updateFinset, Measurable.comp, dite, measurable_updateFinset', measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
x : (i : ↥s) → X (↑i : δ)
⊢ Measurable (β := (i : δ) → X i) fun (x_1 : (i : δ) → X i) ↦ updateFinset (π := X) x_1 s x

Tactic:
measurable_updateFinset'.comp measurable_prodMk_right

Premises used: Function.updateFinset, Measurable.comp, measurable_prodMk_right, dite, measurable_updateFinset'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
f : (a : δ) → X a
a : δ
inst_1 : DecidableEq δ
⊢ Measurable (update (β := X) f a)

Tactic:
measurable_update'.comp measurable_prodMk_left

Premises used: measurable_update', Function.update, Measurable.comp, dite, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
a : δ
inst_1 : DecidableEq δ
x : X a
⊢ Measurable (β := (a : δ) → X a) fun (x_1 : (a : δ) → X a) ↦ update (β := X) x_1 a x

Tactic:
measurable_update'.comp measurable_prodMk_right

Premises used: measurable_update', Function.update, Measurable.comp, measurable_prodMk_right, dite
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
⊢ Measurable (α := (a : δ) → X a) (s.restrict (π := X))

Tactic:
measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.val
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s t : Set δ
hst : s ⊆ t
⊢ Measurable (α := (a : (↑t : Type u_4)) → X (↑a : δ)) (restrict₂ (π := X) (s := s) (t := t) hst)

Tactic:
measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.mk, Set.restrict₂._proof_1, Subtype.val
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Finset δ
⊢ Measurable (α := (i : δ) → X i) (s.restrict (π := X))

Tactic:
measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.val
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s t : Finset δ
hst : s ⊆ t
⊢ Measurable (α := (i : ↥t) → X (↑i : δ)) (restrict₂ (π := X) hst)

Tactic:
measurable_pi_lambda _ fun _ ↦ measurable_pi_apply _

Premises used: measurable_pi_lambda, measurable_pi_apply, Subtype.mk, Finset.restrict₂._proof_1, Subtype.val
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
s : Set α
f : α → γ
hf : Measurable f
⊢ Measurable (s.restrict (π := fun (a : α) ↦ γ) f)

Tactic:
hf.comp measurable_subtype_coe

Premises used: measurable_subtype_coe, Measurable.comp, Set.restrict