awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
s t : Set α
hst : s ⊆ t
f : (↑t : Type u_1) → γ
hf : Measurable f
⊢ Measurable.{u_1, u_3} (α := (↑s : Type u_1)) (β := γ) (restrict₂ (π := fun (x : α) ↦ γ) (s := s) (t := t) hst f)

Tactic:
hf.comp (measurable_inclusion hst)

Premises used: Measurable.comp, Set.restrict₂, measurable_inclusion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
s : Finset α
f : α → γ
hf : Measurable f
⊢ Measurable (s.restrict (π := fun (i : α) ↦ γ) f)

Tactic:
hf.comp measurable_subtype_coe

Premises used: measurable_subtype_coe, Measurable.comp, Finset.restrict
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace γ
s t : Finset α
hst : s ⊆ t
f : ↥t → γ
hf : Measurable f
⊢ Measurable.{u_1, u_3} (α := ↥s) (β := γ) (restrict₂ (π := fun (x : α) ↦ γ) hst f)

Tactic:
hf.comp (measurable_inclusion hst)

Premises used: Measurable.comp, Finset.restrict₂, measurable_inclusion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
i i' : δ
h : i = i'
refl : Measurable ⋯.mp
⊢ Measurable ⋯.mp

Tactic:
cases h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
i : δ
⊢ Measurable ⋯.mp

Tactic:
measurable_id

Premises used: measurable_id, Eq.mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
i : δ
⊢ Measurable ⋯.mp

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)
β : Type u_7
inst_1 : MeasurableSpace β
i i' : δ
h : i = i'
f : β → X i
hf : Measurable f
⊢ Measurable.{u_7, u_6} (β := X i') fun (x : β) ↦ ⋯.mp (f x)

Tactic:
(measurable_eq_mp X h).comp hf

Premises used: Measurable.comp, measurable_eq_mp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
rw :
  ∀ (a : δ),
    Measurable (β := X a) fun (x : (a : δ') → X ((f : (a : δ') → δ) a)) ↦
      (Equiv.piCongrLeft X f : (a : (a : δ') → X ((f : (a : δ') → δ) a)) → (b : δ) → X b) x a
⊢ Measurable (α := (a : δ') → X ((f : (a : δ') → δ) a)) (β := (b : δ) → X b)
    (⇑(Equiv.piCongrLeft X f) : (a : (a : δ') → X ((f : (a : δ') → δ) a)) → (b : δ) → X b)

Tactic:
rw [measurable_pi_iff]

Premises used: measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
simp_rw : Measurable (β := X i) fun (x : (a : δ') → X ((f : (a : δ') → δ) a)) ↦ cast ⋯ (x ((f.symm : (a : δ) → δ') i))
⊢ Measurable (β := X i) fun (x : (a : δ') → X ((f : (a : δ') → δ) a)) ↦
    (Equiv.piCongrLeft X f : (a : (a : δ') → X ((f : (a : δ') → δ) a)) → (b : δ) → X b) x i

Tactic:
simp_rw [Equiv.piCongrLeft_apply_eq_cast]

Premises used: Equiv.piCongrLeft_apply_eq_cast
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
⊢ Measurable (β := X i) fun (x : (a : δ') → X ((f : (a : δ') → δ) a)) ↦ cast ⋯ (x ((f.symm : (a : δ) → δ') i))

Tactic:
Measurable.eq_mp X (f.apply_symm_apply i) <| measurable_pi_apply <| f.symm i

Premises used: Equiv.apply_symm_apply, cast, measurable_pi_apply, Measurable.eq_mp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
⊢ Measurable (β := X i) fun (x : (a : δ') → X ((f : (a : δ') → δ) a)) ↦ cast ⋯ (x ((f.symm : (a : δ) → δ') i))

Tactic:
exact Measurable.eq_mp X (f.apply_symm_apply i) <| measurable_pi_apply <| f.symm i

Premises used: Equiv.apply_symm_apply, measurable_pi_apply, Measurable.eq_mp, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
rw : MeasurableSet (α := (i : δ) → X i) (⋂ a ∈ s, eval (β := X) a ⁻¹' t a)
⊢ MeasurableSet (s.pi (α := X) t)

Tactic:
rw [pi_def]

Premises used: Set.pi_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (α := (i : δ) → X i) (⋂ a ∈ s, eval (β := X) a ⁻¹' t a)

Tactic:
MeasurableSet.biInter hs fun i hi => measurable_pi_apply _ (ht i hi)

Premises used: measurable_pi_apply, MeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
ht : ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (α := (i : δ) → X i) (⋂ a ∈ s, eval (β := X) a ⁻¹' t a)

Tactic:
exact MeasurableSet.biInter hs fun i hi => measurable_pi_apply _ (ht i hi)

Premises used: measurable_pi_apply, MeasurableSet.biInter
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : Countable δ
t : (i : δ) → Set (X i)
ht : ∀ (i : δ), MeasurableSet (t i)
⊢ MeasurableSet (pi (α := X) univ t)

Tactic:
MeasurableSet.pi (to_countable _) fun i _ => ht i

Premises used: Set.to_countable, MeasurableSet.pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : Countable δ
t : (i : δ) → Set (X i)
ht : ∀ (i : δ), MeasurableSet (t i)
⊢ pi (α := X) univ t = {f : (i : δ) → X i | ∀ (i : δ), f i ∈ t i}

Tactic:
grind
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi (α := X) t).Nonempty
rcases :
  ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t), MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)
⊢ MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
rcases h with ⟨f, hf⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
⊢ MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩

Premises used: Iff.intro, MeasurableSet.pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
refine : ∀ (hst : MeasurableSet (s.pi (α := X) t)) (i : δ) (hi : i ∈ s), MeasurableSet (t i)
⊢ MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
hst : MeasurableSet (s.pi (α := X) t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (update (β := X) f i ⁻¹' s.pi (α := X) t)

Tactic:
measurable_update f (a := i) hst

Premises used: measurable_update
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
hst : MeasurableSet (s.pi (α := X) t)
i : δ
hi : i ∈ s
h : t i = update (β := X) f i ⁻¹' s.pi (α := X) t
⊢ MeasurableSet (t i)

Tactic:
convert! measurable_update f (a := i) hst

Premises used: measurable_update
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
hst : MeasurableSet (s.pi (α := X) t)
i : δ
hi : i ∈ s
h : ∀ j ∈ s, j ≠ i → f j ∈ t j
⊢ t i = update (β := X) f i ⁻¹' s.pi (α := X) t

Tactic:
rw [update_preimage_pi hi]

Premises used: Set.update_preimage_pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
hst : MeasurableSet (s.pi (α := X) t)
i : δ
hi : i ∈ s
⊢ ∀ j ∈ s, j ≠ i → f j ∈ t j

Tactic:
fun j hj _ => hf j hj
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi (α := X) t
hst : MeasurableSet (s.pi (α := X) t)
i : δ
hi : i ∈ s
⊢ ∀ j ∈ s, j ≠ i → f j ∈ t j

Tactic:
exact fun j hj _ => hf j hj
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi (α := X) t).Nonempty
rcases :
  ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t), MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)
rcases₁ :
  ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t) (hst : MeasurableSet (s.pi (α := X) t)) (i : δ) (hi : i ∈ s),
    MeasurableSet (t i)
h₁ :
  ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t) (hst : MeasurableSet (s.pi (α := X) t)) (i : δ) (hi : i ∈ s),
    t i = update (β := X) f i ⁻¹' s.pi (α := X) t
h₂ :
  ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t) (hst : MeasurableSet (s.pi (α := X) t)) (i : δ) (hi : i ∈ s),
    ∀ j ∈ s, j ≠ i → f j ∈ t j
⊢ MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
classical
    rcases h with ⟨f, hf⟩
    refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩
    convert! measurable_update f (a := i) hst
    rw [update_preimage_pi hi]
    exact fun j hj _ => hf j hj
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
inl :
  ∀ (h : s.pi (α := X) t = ∅), MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅
inr :
  ∀ (h : (s.pi (α := X) t).Nonempty),
    MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅
⊢ MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅

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

Premises used: Set.eq_empty_or_nonempty, Set.pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : s.pi (α := X) t = ∅
⊢ MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
h : (s.pi (α := X) t).Nonempty
⊢ MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅

Tactic:
simp [measurableSet_pi_of_nonempty hs, h, ← not_nonempty_iff_eq_empty]

Premises used: measurableSet_pi_of_nonempty, Set.not_nonempty_iff_eq_empty
-- 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 α
X : δ → Type u_6
inst : MeasurableSpace α
inst_1 : (a : δ) → MeasurableSpace (X a)
inst_2 : MeasurableSpace γ
inst_3 : Countable δ
inst_4 : ∀ (a : δ), MeasurableSingletonClass.{u_6} (X a)
⊢ MeasurableSingletonClass ((a : δ) → X a)

Tactic:
⟨fun f => univ_pi_singleton f ▸ MeasurableSet.univ_pi fun t => measurableSet_singleton (f t)⟩

Premises used: MeasurableSingletonClass.measurableSet_singleton, Eq.rec, MeasurableSingletonClass.mk, Set.univ_pi_singleton, MeasurableSet.univ_pi
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
⊢ Measurable (α := ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) (β := (i : δ) → X i)
    (⇑(Equiv.piEquivPiSubtypeProd p X).symm :
      (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)

Tactic:
measurable_pi_iff.2 fun j => ?_

Premises used: Iff.mpr, measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
refine :
  ∀ (j : δ),
    Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
      ((Equiv.piEquivPiSubtypeProd p X).symm :
          (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)
        x j
⊢ Measurable (α := ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) (β := (i : δ) → X i)
    (⇑(Equiv.piEquivPiSubtypeProd p X).symm :
      (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)

Tactic:
refine measurable_pi_iff.2 fun j => ?_

Premises used: Iff.mpr, measurable_pi_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
pos :
  ∀ (hj : p j),
    Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
      ((Equiv.piEquivPiSubtypeProd p X).symm :
          (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)
        x j
neg :
  ∀ (hj : ¬p j),
    Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
      ((Equiv.piEquivPiSubtypeProd p X).symm :
          (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)
        x j
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    ((Equiv.piEquivPiSubtypeProd p X).symm :
        (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)
      x j

Tactic:
by_cases hj : p j
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : p j
pos :
  Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    x.1 (Subtype.mk (p := fun (x : δ) ↦ p x) j ⋯)
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    ((Equiv.piEquivPiSubtypeProd p X).symm :
        (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)
      x j

Tactic:
simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]

Premises used: dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : p j
⊢ Measurable (β := X (↑(Subtype.mk (p := fun (x : δ) ↦ p x) j hj) : δ)) fun (f : (i : { x : δ // p x }) → X (↑i : δ)) ↦
    f (Subtype.mk (p := fun (x : δ) ↦ p x) j hj)

Tactic:
have : Measurable fun (f : ∀ i : { x // p x }, X i.1) => f ⟨j, hj⟩ :=
      measurable_pi_apply (X := fun i : {x // p x} => X i.1) ⟨j, hj⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : p j
this :
  Measurable (β := X (↑(Subtype.mk (p := fun (x : δ) ↦ p x) j hj) : δ)) fun (f : (i : { x : δ // p x }) → X (↑i : δ)) ↦
    f (Subtype.mk (p := fun (x : δ) ↦ p x) j hj)
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    x.1 (Subtype.mk (p := fun (x : δ) ↦ p x) j ⋯)

Tactic:
Measurable.comp this measurable_fst

Premises used: Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : p j
this :
  Measurable (β := X (↑(Subtype.mk (p := fun (x : δ) ↦ p x) j hj) : δ)) fun (f : (i : { x : δ // p x }) → X (↑i : δ)) ↦
    f (Subtype.mk (p := fun (x : δ) ↦ p x) j hj)
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    x.1 (Subtype.mk (p := fun (x : δ) ↦ p x) j ⋯)

Tactic:
exact Measurable.comp this measurable_fst

Premises used: Measurable.comp, measurable_fst
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : ¬p j
neg :
  Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    x.2 (Subtype.mk (p := fun (x : δ) ↦ ¬p x) j ⋯)
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    ((Equiv.piEquivPiSubtypeProd p X).symm :
        (a : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) → (i : δ) → X i)
      x j

Tactic:
simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]

Premises used: dif_neg, Equiv.piEquivPiSubtypeProd_symm_apply, not_false_iff
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : ¬p j
⊢ Measurable (β := X (↑(Subtype.mk (p := fun (x : δ) ↦ ¬p x) j hj) : δ))
    fun (f : (i : { x : δ // ¬p x }) → X (↑i : δ)) ↦ f (Subtype.mk (p := fun (x : δ) ↦ ¬p x) j hj)

Tactic:
have : Measurable fun (f : ∀ i : { x // ¬p x }, X i.1) => f ⟨j, hj⟩ :=
      measurable_pi_apply (X := fun i : {x // ¬p x} => X i.1) ⟨j, hj⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : ¬p j
this :
  Measurable (β := X (↑(Subtype.mk (p := fun (x : δ) ↦ ¬p x) j hj) : δ))
    fun (f : (i : { x : δ // ¬p x }) → X (↑i : δ)) ↦ f (Subtype.mk (p := fun (x : δ) ↦ ¬p x) j hj)
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    x.2 (Subtype.mk (p := fun (x : δ) ↦ ¬p x) j ⋯)

Tactic:
Measurable.comp this measurable_snd

Premises used: Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
j : δ
hj : ¬p j
this :
  Measurable (β := X (↑(Subtype.mk (p := fun (x : δ) ↦ ¬p x) j hj) : δ))
    fun (f : (i : { x : δ // ¬p x }) → X (↑i : δ)) ↦ f (Subtype.mk (p := fun (x : δ) ↦ ¬p x) j hj)
⊢ Measurable (β := X j) fun (x : ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ))) ↦
    x.2 (Subtype.mk (p := fun (x : δ) ↦ ¬p x) j ⋯)

Tactic:
exact Measurable.comp this measurable_snd

Premises used: Measurable.comp, measurable_snd
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred p
⊢ Measurable (α := (i : δ) → X i) (β := ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ)))
    (⇑(Equiv.piEquivPiSubtypeProd p X) :
      (a : (i : δ) → X i) → ((i : { x : δ // p x }) → X (↑i : δ)) × ((i : { x : δ // ¬p x }) → X (↑i : δ)))

Tactic:
(measurable_pi_iff.2 fun _ => measurable_pi_apply _).prodMk
    (measurable_pi_iff.2 fun _ => measurable_pi_apply _)

Premises used: Iff.mpr, measurable_pi_iff, measurable_pi_apply, Measurable.prodMk, Subtype.val
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
⊢ Measurable (α := (i : δ) → X i) (β := TProd X []) (TProd.mk (α := X) [])

Tactic:
measurable_const

Premises used: measurable_const, List.TProd.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
⊢ Measurable (α := (i : δ) → X i) (β := TProd X []) (TProd.mk (α := X) [])

Tactic:
exact measurable_const

Premises used: measurable_const
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
i : δ
l : List δ
ih : Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)
⊢ Measurable (α := (i : δ) → X i) (TProd.mk (α := X) (i :: l))

Tactic:
(measurable_pi_apply i).prodMk ih

Premises used: measurable_pi_apply, Measurable.prodMk, List.foldr, List.TProd.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
i : δ
l : List δ
ih : Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)
⊢ Measurable (α := (i : δ) → X i) (TProd.mk (α := X) (i :: l))

Tactic:
exact (measurable_pi_apply i).prodMk ih

Premises used: measurable_pi_apply, Measurable.prodMk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
nil : Measurable (α := (i : δ) → X i) (β := TProd X []) (TProd.mk (α := X) [])
cons :
  ∀ (i : δ) (l : List δ) (ih : Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)),
    Measurable (α := (i : δ) → X i) (TProd.mk (α := X) (i :: l))
⊢ Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)

Tactic:
induction l with
  | nil => exact measurable_const
  | cons i l ih => exact (measurable_pi_apply i).prodMk ih

Premises used: List.cons, measurable_const, List.nil
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
pos : ∀ (hji : j = i), Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
neg : ∀ (hji : ¬j = i), Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj

Tactic:
by_cases hji : j = i
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
pos : ∀ (hj : j ∈ j :: is), Measurable (β := X j) fun (v : TProd X (j :: is)) ↦ v.elim (α := X) hj
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj

Tactic:
subst hji
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable (β := X j) fun (v : TProd X (j :: is)) ↦ v.elim (α := X) hj

Tactic:
simpa using measurable_fst

Premises used: measurable_fst