awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s,
      p < q →
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : Encodable (↑s : Type u_2)
u v : (p q : β) → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x : α | f x < p} ⊆ u p q ∧
          {x : α | q < f x} ⊆ v p q ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))
u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β :=
  fun (x : α) ↦
    ⨅ (i : (↑s : Type u_2)), (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)
μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
i : (↑s : Type u_2)
H : x ∈ u' (↑i : β)
hx : (↑i : β) < f x
r : β
rs : r ∈ s
xr : (↑i : β) < r
rq : r < f x
A : x ∈ v (↑i : β) r
⊢ Membership.mem (γ := Set α) (⋃ (q : (↑(s ∩ Ioi (↑i : β)) : Type u_2)), u' (↑i : β) ∩ v (↑i : β) (↑q : β)) x
have pos : x ∈ u' (↑i : β) ∩ v (↑i : β) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ s ∩ Ioi (↑i : β)) r sorry) : β)
Tactic: refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s,
      p < q →
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : Encodable (↑s : Type u_2)
u v : (p q : β) → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x : α | f x < p} ⊆ u p q ∧
          {x : α | q < f x} ⊆ v p q ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))
u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β :=
  fun (x : α) ↦
    ⨅ (i : (↑s : Type u_2)), (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)
μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
q : β
hq : f x < q
⊢ ∃ (i : (↑s : Type u_2)),
    (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x < q
have obtain : ∀ (r : β) (rs : r ∈ s) (xr : f x < r) (rq : r < q),
  ∃ (i : (↑s : Type u_2)),
    (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x < q
Tactic: obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s :=
        dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s,
      p < q →
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : Encodable (↑s : Type u_2)
u v : (p q : β) → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x : α | f x < p} ⊆ u p q ∧
          {x : α | q < f x} ⊆ v p q ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))
u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β :=
  fun (x : α) ↦
    ⨅ (i : (↑s : Type u_2)), (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)
μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
q : β
hq : f x < q
r : β
rs : r ∈ s
xr : f x < r
rq : r < q
⊢ ∃ (i : (↑s : Type u_2)),
    (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x < q
have refine : (u' (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ s) r rs) : β)).piecewise (β := fun (x : α) ↦ β)
    (fun (x : α) ↦ (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ s) r rs) : β)) (fun (x : α) ↦ ⊤) x <
  q
Tactic: refine ⟨⟨r, rs⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s,
      p < q →
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
this_1 : Encodable (↑s : Type u_2)
u v : (p q : β) → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x : α | f x < p} ⊆ u p q ∧
          {x : α | q < f x} ⊆ v p q ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))
u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β :=
  fun (x : α) ↦
    ⨅ (i : (↑s : Type u_2)), (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)
μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
this : ∀ᵐ (x : α) ∂μ, x ∉ t
x : α
hx : x ∉ t
q : β
hq : f x < q
r : β
rs : r ∈ s
xr : f x < r
rq : r < q
⊢ (u' (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ s) r rs) : β)).piecewise (β := fun (x : α) ↦ β)
      (fun (x : α) ↦ (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ s) r rs) : β)) (fun (x : α) ↦ ⊤) x <
    q
have A : x ∈ u' r
Tactic: have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : CompleteLinearOrder β
inst_1 : DenselyOrdered β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
inst_4 : SecondCountableTopology β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s,
      p < q →
        ∃ (u : Set α) (v : Set α),
          MeasurableSet u ∧
            MeasurableSet v ∧
              {x : α | f x < p} ⊆ u ∧
                {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
this : Encodable (↑s : Type u_2)
u v : (p q : β) → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x : α | f x < p} ⊆ u p q ∧
          {x : α | q < f x} ⊆ v p q ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u p q ∩ v p q) : ℝ≥0∞) (0 : ℝ≥0∞))
u' : β → Set α := fun (p : β) ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β :=
  fun (x : α) ↦
    ⨅ (i : (↑s : Type u_2)), (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ (p : (↑s : Type u_2)), ⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)
μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEMeasurable f μ
have ff' : ∀ᵐ (x : α) ∂μ, f x = f' x
Tactic: have ff' : ∀ᵐ x ∂μ, f x = f' x := by
    have : ∀ᵐ x ∂μ, x ∉ t := by
      have : μ t = 0 := le_antisymm μt bot_le
      change μ _ = 0
      convert! this
      ext y
      simp only [mem_setOf_eq, mem_compl_iff, not_notMem]
    filter_upwards [this] with x hx
    apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
    · intro i
      by_cases H : x ∈ u' i
      swap
      · simp only [H, le_top, not_false_iff, piecewise_eq_of_notMem]
      simp only [H, piecewise_eq_of_mem]
      contrapose! hx
      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (i : β) (f x) ∩ s :=
        dense_iff_inter_open.1 s_dense (Ioo i (f x)) isOpen_Ioo (nonempty_Ioo.2 hx)
      have A : x ∈ v i r := (huv i r).2.2.2.1 rq
      refine mem_iUnion.2 ⟨i, ?_⟩
      refine mem_iUnion.2 ⟨⟨r, ⟨rs, xr⟩⟩, ?_⟩
      exact ⟨H, A⟩
    · intro q hq
      obtain ⟨r, ⟨xr, rq⟩, rs⟩ : ∃ r, r ∈ Ioo (f x) q ∩ s :=
        dense_iff_inter_open.1 s_dense (Ioo (f x) q) isOpen_Ioo (nonempty_Ioo.2 hq)
      refine ⟨⟨r, rs⟩, ?_⟩
      have A : x ∈ u' r := mem_biInter fun i _ => (huv r i).2.2.1 xr
      simp only [A, rq, piecewise_eq_of_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q →
      ∃ (u : Set α) (v : Set α),
        MeasurableSet u ∧
          MeasurableSet v ∧
            {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
              {x : α | (↑q : ℝ≥0∞) < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ AEMeasurable f μ
have obtain : ∀ (s : Set ℝ≥0∞) (s_count : s.Countable) (s_dense : Dense s), 0 ∉ s → ∀ (s_top : ∞ ∉ s), AEMeasurable f μ
Tactic: obtain ⟨s, s_count, s_dense, _, s_top⟩ :
    ∃ s : Set ℝ≥0∞, s.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s :=
    ENNReal.exists_countable_dense_no_zero_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q →
      ∃ (u : Set α) (v : Set α),
        MeasurableSet u ∧
          MeasurableSet v ∧
            {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
              {x : α | (↑q : ℝ≥0∞) < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
left : 0 ∉ s
s_top : ∞ ∉ s
⊢ AEMeasurable f μ
have I : ∀ x ∈ s, x ≠ ∞
Tactic: have I : ∀ x ∈ s, x ≠ ∞ := fun x xs hx => s_top (hx ▸ xs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q →
      ∃ (u : Set α) (v : Set α),
        MeasurableSet u ∧
          MeasurableSet v ∧
            {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
              {x : α | (↑q : ℝ≥0∞) < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
left : 0 ∉ s
s_top : ∞ ∉ s
I : ∀ x ∈ s, x ≠ ∞
⊢ AEMeasurable f μ
have apply : ∀ p ∈ s,
  ∀ q ∈ s,
    p < q →
      ∃ (u : Set α) (v : Set α),
        MeasurableSet u ∧
          MeasurableSet v ∧
            {x : α | f x < p} ⊆ u ∧
              {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets μ s s_count s_dense _
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q →
      ∃ (u : Set α) (v : Set α),
        MeasurableSet u ∧
          MeasurableSet v ∧
            {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
              {x : α | (↑q : ℝ≥0∞) < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
left : 0 ∉ s
s_top : ∞ ∉ s
I : ∀ x ∈ s, x ≠ ∞
p : ℝ≥0∞
hp : p ∈ s
q : ℝ≥0∞
hq : q ∈ s
hpq : p < q
⊢ ∃ (u : Set α) (v : Set α),
    MeasurableSet u ∧
      MeasurableSet v ∧
        {x : α | f x < p} ⊆ u ∧
          {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
have lift : ∀ (p : ℝ≥0) (hp : (↑p : ℝ≥0∞) ∈ s) (hpq : (↑p : ℝ≥0∞) < q),
  ∃ (u : Set α) (v : Set α),
    MeasurableSet u ∧
      MeasurableSet v ∧
        {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
          {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: lift p to ℝ≥0 using I p hp
Cleared hypotheses: p, hp, hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableOrder (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h :
  ∀ (p q : ℝ≥0),
    p < q →
      ∃ (u : Set α) (v : Set α),
        MeasurableSet u ∧
          MeasurableSet v ∧
            {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
              {x : α | (↑q : ℝ≥0∞) < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
s : Set ℝ≥0∞
s_count : s.Countable
s_dense : Dense s
left : 0 ∉ s
s_top : ∞ ∉ s
I : ∀ x ∈ s, x ≠ ∞
q : ℝ≥0∞
hq : q ∈ s
p : ℝ≥0
hp : (↑p : ℝ≥0∞) ∈ s
hpq : (↑p : ℝ≥0∞) < q
⊢ ∃ (u : Set α) (v : Set α),
    MeasurableSet u ∧
      MeasurableSet v ∧
        {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
          {x : α | q < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
have lift : ∀ (q : ℝ≥0) (hq : (↑q : ℝ≥0∞) ∈ s) (hpq : (↑p : ℝ≥0∞) < (↑q : ℝ≥0∞)),
  ∃ (u : Set α) (v : Set α),
    MeasurableSet u ∧
      MeasurableSet v ∧
        {x : α | f x < (↑p : ℝ≥0∞)} ⊆ u ∧
          {x : α | (↑q : ℝ≥0∞) < f x} ⊆ v ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: lift q to ℝ≥0 using I q hq
Cleared hypotheses: q, hq, hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeqSet hf p ⊆ {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}
have rw : {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x}ᶜ ⊆
  toMeasurable μ {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x) ∧ p x fun (n : ι) ↦ f n x}ᶜ
Tactic: rw [aeSeqSet, ← compl_compl { x | ∀ i, f i x = (hf i).mk (f i) x }, Set.compl_subset_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}ᶜ ⊆
    toMeasurable μ {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ
have refine : ∀ (x : α)
  (h :
    Membership.mem (γ := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x) ∧ p x fun (n : ι) ↦ f n x} x),
  Membership.mem (γ := Set α) {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x} x
Tactic: refine Set.Subset.trans (Set.compl_subset_compl.mpr fun x h => ?_) (subset_toMeasurable _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun (n : ι) ↦ aeSeq hf p n x
have simp : p x fun (n : ι) ↦ AEMeasurable.mk (f n) sorry x
Tactic: simp only [aeSeq, hx, if_true]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun (n : ι) ↦ AEMeasurable.mk (f n) ⋯ x
have rw : p x fun (n : ι) ↦ f n x
Tactic: rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}
have rw : {x : α | p x fun (n : ι) ↦ f n x}ᶜ ⊆
  toMeasurable μ {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x) ∧ p x fun (n : ι) ↦ f n x}ᶜ
Tactic: rw [← compl_compl { x | p x fun n => f n x }, aeSeqSet, Set.compl_subset_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ {x : α | p x fun (n : ι) ↦ f n x}ᶜ ⊆
    toMeasurable μ {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ
have refine : Subset.{u_2} (α := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x) ∧ p x fun (n : ι) ↦ f n x}
  {x : α | p x fun (n : ι) ↦ f n x}
Tactic: refine Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun (n : ι) ↦ f n x
have have : ∀ (h_ss : aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}), p x fun (n : ι) ↦ f n x
Tactic: have h_ss : aeSeqSet hf p ⊆ { x | p x fun n => f n x } := by
    rw [← compl_compl { x | p x fun n => f n x }, aeSeqSet, Set.compl_subset_compl]
    refine Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)
    exact fun x hx => hx.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}
⊢ p x fun (n : ι) ↦ f n x
have hx' : Membership.mem (γ := Set α) {x : α | p x fun (n : ι) ↦ f n x} x
Tactic: have hx' := Set.mem_of_subset_of_mem h_ss hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun (n : ι) ↦ f n x
have have : ∀ (h_eq : Eq (α := (n : ι) → β) (fun (n : ι) ↦ f n x) fun (n : ι) ↦ aeSeq hf p n x), p x fun (n : ι) ↦ f n x
Tactic: have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x :=
    funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : Eq (α := (n : ι) → β) (fun (n : ι) ↦ f n x) fun (n : ι) ↦ aeSeq hf p n x
⊢ p x fun (n : ι) ↦ f n x
have rw : p x fun (n : ι) ↦ aeSeq hf p n x
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (aeSeqSet hf p)ᶜ : ENNReal) (0 : ENNReal)
have rw : Eq (α := ENNReal)
  ((μ : (a : Set α) → ENNReal) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) sorry x) ∧ p x fun (n : ι) ↦ f n x}ᶜ :
    ENNReal)
  (0 : ENNReal)
Tactic: rw [aeSeqSet, compl_compl, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have hf_eq : ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) sorry
Tactic: have hf_eq := fun i => (hf i).ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
hf_eq : ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) ⋯
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have hf_eq₁ : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) sorry a
Tactic: simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq
Cleared hypotheses: hf_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ Filter.EventuallyEq.{u_2, u_3} (β := β) (ae μ) (⨆ (n : ι), aeSeq hf p n) (⨆ (n : ι), f n)
have simp_rw : Eq (α := ENNReal)
  ((μ : (a : Set α) → ENNReal) {a : α | ¬Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} :
    ENNReal)
  (0 : ENNReal)
Tactic: simp_rw [Filter.EventuallyEq, ae_iff, iSup_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEMeasurableSequence (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ Membership.mem (γ := Set α) {a : α | Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} x
have e_s : Eq (α := ι → β) (fun (i : ι) ↦ aeSeq hf p i x) fun (i : ι) ↦ f i x
Tactic: congr