awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : Unique δ
⊢ Measurable (α := X default) (uniqueElim (α := X))
have simp_rw : Measurable (β := X default) fun (x : X default) ↦ x
Tactic: simp_rw [measurable_pi_iff, Unique.forall_iff, uniqueElim_default]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
inst_1 : DecidableEq δ
s : Finset δ
⊢ Measurable (β := (i : δ) → X i) fun (p : ((i : δ) → X i) × ((i : ↥s) → X (↑i : δ))) ↦ updateFinset (π := X) p.1 s p.2
have 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
Tactic: simp only [updateFinset, 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)
inst_1 : DecidableEq δ
s : Finset δ
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
have 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
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ 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
have 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
Tactic: by_cases h : i ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
i i' : δ
h : i = i'
⊢ Measurable ⋯.mp
have refl : Measurable sorry.mp
Tactic: cases h
Cleared hypotheses: i', h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
⊢ Measurable (α := (a : δ') → X ((f : (a : δ') → δ) a)) (β := (b : δ) → X b)
    (⇑(Equiv.piCongrLeft X f) : (a : (a : δ') → X ((f : (a : δ') → δ) a)) → (b : δ) → X b)
have 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
Tactic: rw [measurable_pi_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)) ↦
    (Equiv.piCongrLeft X f : (a : (a : δ') → X ((f : (a : δ') → δ) a)) → (b : δ) → X b) x i
have simp_rw : Measurable (β := X i) fun (x : (a : δ') → X ((f : (a : δ') → δ) a)) ↦ cast sorry (x ((f.symm : (a : δ) → δ') i))
Tactic: simp_rw [Equiv.piCongrLeft_apply_eq_cast]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 (s.pi (α := X) t)
have rw : MeasurableSet (α := (i : δ) → X i) (⋂ a ∈ s, eval (β := X) a ⁻¹' t a)
Tactic: rw [pi_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
have rcases : ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t), MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)
Tactic: rcases h with ⟨f, hf⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
have refine : ∀ (hst : MeasurableSet (s.pi (α := X) t)) (i : δ) (hi : i ∈ s), MeasurableSet (t i)
Tactic: refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 (t i)
have h : t i = update (β := X) f i ⁻¹' s.pi (α := X) t
Tactic: convert! measurable_update f (a := i) hst
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ t i = update (β := X) f i ⁻¹' s.pi (α := X) t
have h : ∀ j ∈ s, j ≠ i → f j ∈ t j
Tactic: rw [update_preimage_pi hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
have rcases : ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t), 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
have rcases₁ : ∀ (f : (i : δ) → X i) (hf : f ∈ s.pi (α := X) t) (hst : MeasurableSet (s.pi (α := X) t)) (i : δ) (hi : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
⊢ MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ MeasurableSet (s.pi (α := X) t) ↔ ∀ i ∈ s, MeasurableSet (t i)
have 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
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
⊢ MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅
have inl : ∀ (h : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 = ∅
⊢ MeasurableSet (s.pi (α := X) t) ↔ (∀ i ∈ s, MeasurableSet (t i)) ∨ s.pi (α := X) t = ∅
have inr : ∀ (h : (s.pi (α := X) t).Nonempty),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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)
have 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
Tactic: refine measurable_pi_iff.2 fun j => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (a : δ) → MeasurableSpace (X a)
p : δ → Prop
inst_1 : DecidablePred 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
have 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
Tactic: by_cases hj : p j
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ 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
have 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
Tactic: by_cases hj : p j
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 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
have 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 sorry)
Tactic: simp only [hj, dif_pos, Equiv.piEquivPiSubtypeProd_symm_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
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 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 ⋯)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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 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
have 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 sorry)
Tactic: simp only [hj, Equiv.piEquivPiSubtypeProd_symm_apply, dif_neg, not_false_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (hypothesis)
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 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 ⋯)
have 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)
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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
⊢ Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)
have nil : Measurable (α := (i : δ) → X i) (β := TProd X []) (TProd.mk (α := X) [])
Tactic: induction l with
  | nil => exact measurable_const
  | cons i l ih => exact (measurable_pi_apply i).prodMk ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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) [])
⊢ Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)
have cons : ∀ (i : δ) (l : List δ) (ih : Measurable (α := (i : δ) → X i) (TProd.mk (α := X) l)),
  Measurable (α := (i : δ) → X i) (TProd.mk (α := X) (i :: l))
Tactic: induction l with
  | nil => exact measurable_const
  | cons i l ih => exact (measurable_pi_apply i).prodMk ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
inst_1 : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
have pos : ∀ (hji : j = i), Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
have neg : ∀ (hji : ¬j = i), Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
Tactic: by_cases hji : j = i
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
have pos : ∀ (hj : j ∈ j :: is), Measurable (β := X j) fun (v : TProd X (j :: is)) ↦ v.elim (α := X) hj
Tactic: subst hji
Cleared hypotheses: i, hj, hji
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ v.elim (α := X) hj
have neg : Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 sorry
Tactic: simp only [TProd.elim_of_ne _ hji]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
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
⊢ Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 ⋯
have neg : ∀ (hj_1 : j = i ∨ j ∈ is) (hji : ¬j = i), Measurable (β := X j) fun (v : TProd X (i :: is)) ↦ TProd.elim (α := X) v.2 sorry
Tactic: rw [mem_cons] at hj
Cleared hypotheses: hji
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
⊢ MeasurableSet (Set.tprod (α := X) l s)
have nil : MeasurableSet (α := TProd X []) (Set.tprod (α := X) [] s)
Tactic: induction l with
  | nil => exact MeasurableSet.univ
  | cons i l ih => exact (hs i).prod ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
δ : Type u_4
X : δ → Type u_6
inst : (i : δ) → MeasurableSpace (X i)
l : List δ
s : (i : δ) → Set (X i)
hs : ∀ (i : δ), MeasurableSet (s i)
nil : MeasurableSet (α := TProd X []) (Set.tprod (α := X) [] s)
⊢ MeasurableSet (Set.tprod (α := X) l s)
have cons : ∀ (i : δ) (l : List δ) (ih : MeasurableSet (Set.tprod (α := X) l s)), MeasurableSet (Set.tprod (α := X) (i :: l) s)
Tactic: induction l with
  | nil => exact MeasurableSet.univ
  | cons i l ih => exact (hs i).prod ih
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
⊢ MeasurableSet (α := α ⊕ β) (range Sum.inl)
have rw : MeasurableSet (α := α ⊕ β) (Sum.inl '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace α
⊢ MeasurableSet (α := α ⊕ β) (range Sum.inr)
have rw : MeasurableSet (α := α ⊕ β) (Sum.inr '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p q : α → Prop
hp : Measurable p
hq : Measurable q
⊢ MeasurableSet.{u_1} (α := α) {a : α | p a ↔ q a}
have simp_rw : MeasurableSet.{u_1} (α := α) {a : α | (p a → q a) ∧ (q a → p a)}
Tactic: simp_rw [iff_iff_implies_and_implies]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (i : ι), p i a}
have rw : MeasurableSet.{u_1} (α := α) (⋂ (i : ι), {x : α | p i x})
Tactic: rw [setOf_forall]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
ι : Sort uι
inst : MeasurableSpace α
inst_1 : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∃ (i : ι), p i a}
have rw : MeasurableSet.{u_1} (α := α) (⋃ (i : ι), {x : α | p i x})
Tactic: rw [setOf_exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| Measurable (β := Prop) fun (x : α) ↦ a = f x
have h : ∀ (x : α), a = f x
Tactic: enter [1, x]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
x_1 : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
x : α
| a = f x
have h : f x = a
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
| Measurable (β := Prop) fun (x : α) ↦ a = f x
have h : ∀ (x : α), f x = a
Tactic: enter [1, x]; rw [eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
f : α → β
hf : Measurable f
a : β
⊢ Measurable (β := Prop) fun (x : α) ↦ a = f x
have conv : Measurable (β := Prop) fun (x : α) ↦ f x = a
Tactic: conv => enter [1, x]; rw [eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.MeasurableSpace.Constructions (goal)
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Measurable (α := (x : ι) → (y : κ x) → X x y) (Sigma.uncurry (β := κ) (γ := X))
have refine : ∀ (x : Sigma κ),
  Measurable (β := X (x.fst (β := κ)) (x.snd (β := κ))) fun (c : (x : ι) → (y : κ x) → X x y) ↦
    Sigma.uncurry (β := κ) (γ := X) c x
Tactic: refine measurable_pi_lambda _ fun _ ↦ ?_