awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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
A : x ∈ u' r
⊢ (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:
simp only [A, rq, piecewise_eq_of_mem]

Premises used: Set.piecewise_eq_of_mem
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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∞)
⊢ ∀ᵐ (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]
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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∞)
ff' : ∀ᵐ (x : α) ∂μ, f x = f' x
⊢ AEMeasurable f μ

Tactic:
⟨f', f'_meas, ff'⟩

Premises used: AEMeasurable, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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∞)
ff' : ∀ᵐ (x : α) ∂μ, f x = f' x
⊢ AEMeasurable f μ

Tactic:
exact ⟨f', f'_meas, ff'⟩
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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.Countable ∧ Dense s ∧ 0 ∉ s ∧ ∞ ∉ s

Tactic:
ENNReal.exists_countable_dense_no_zero_top

Premises used: ENNReal.exists_countable_dense_no_zero_top
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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∞)
obtain : ∀ (s : Set ℝ≥0∞) (s_count : s.Countable) (s_dense : Dense s), 0 ∉ s → ∀ (s_top : ∞ ∉ s), AEMeasurable f μ
⊢ 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

Premises used: ENNReal, ENNReal.exists_countable_dense_no_zero_top, Set
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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
⊢ ∀ x ∈ s, x ≠ ∞

Tactic:
have I : ∀ x ∈ s, x ≠ ∞ := fun x xs hx => s_top (hx ▸ xs)
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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 ≠ ∞
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∞)
⊢ AEMeasurable f μ

Tactic:
apply MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets μ s s_count s_dense _

Premises used: MeasureTheory.aemeasurable_of_exist_almost_disjoint_supersets
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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
⊢ p ≠ ∞

Tactic:
I p hp
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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
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∞)
⊢ ∃ (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:
lift p to ℝ≥0 using I p hp
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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
⊢ q ≠ ∞

Tactic:
I q hq
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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
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∞)
⊢ ∃ (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 q to ℝ≥0 using I q hq
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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 : ℝ≥0∞) ∈ s
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:
h p q (ENNReal.coe_lt_coe.1 hpq)

Premises used: setOf, ENNReal.coe_lt_coe, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder
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 : ℝ≥0∞) ∈ s
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:
exact h p q (ENNReal.coe_lt_coe.1 hpq)

Premises used: ENNReal.coe_lt_coe, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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 : ι
rw :
  {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}ᶜ
⊢ aeSeqSet hf p ⊆ {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}

Tactic:
rw [aeSeqSet, ← compl_compl { x | ∀ i, f i x = (hf i).mk (f i) x }, Set.compl_subset_compl]

Premises used: compl_compl, setOf, Set.compl_subset_compl, aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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}ᶜ

Tactic:
Set.Subset.trans (Set.compl_subset_compl.mpr fun x h => ?_) (subset_toMeasurable _ _)

Premises used: Iff.mpr, Set.Subset.trans, MeasureTheory.subset_toMeasurable, Set.compl_subset_compl
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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 : ι
refine :
  ∀ (x : α)
    (h :
      Membership.mem (γ := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x} x),
    Membership.mem (γ := Set α) {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x} x
⊢ {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}ᶜ

Tactic:
refine Set.Subset.trans (Set.compl_subset_compl.mpr fun x h => ?_) (subset_toMeasurable _ _)

Premises used: Iff.mpr, Set.Subset.trans, MeasureTheory.subset_toMeasurable, Set.compl_subset_compl
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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_1 : α
hx : x_1 ∈ aeSeqSet hf p
i : ι
x : α
h : Membership.mem (γ := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x} x
⊢ Membership.mem (γ := Set α) {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x} x

Tactic:
h.1

Premises used: Set.Mem, setOf, And.left
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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_1 : α
hx : x_1 ∈ aeSeqSet hf p
i : ι
x : α
h : Membership.mem (γ := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x} x
⊢ Membership.mem (γ := Set α) {x : α | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x} x

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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 : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x

Tactic:
simp only [aeSeq, hx, if_true]

Premises used: if_true, aeSeq
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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 : ι
⊢ aeSeq hf p i x = f i x

Tactic:
simp only [aeSeq_eq_mk_of_mem_aeSeqSet hf hx i, mk_eq_fun_of_mem_aeSeqSet hf hx i]

Premises used: aeSeq.mk_eq_fun_of_mem_aeSeqSet, aeSeq.aeSeq_eq_mk_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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
simp : p x fun (n : ι) ↦ AEMeasurable.mk (f n) ⋯ x
⊢ p x fun (n : ι) ↦ aeSeq hf p n x

Tactic:
simp only [aeSeq, hx, if_true]

Premises used: if_true, aeSeq
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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
rw : p x fun (n : ι) ↦ f n x
⊢ p x fun (n : ι) ↦ AEMeasurable.mk (f n) ⋯ x

Tactic:
rw [funext fun n => mk_eq_fun_of_mem_aeSeqSet hf hx n]

Premises used: aeSeq.mk_eq_fun_of_mem_aeSeqSet, funext
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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
rw :
  {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}ᶜ
⊢ aeSeqSet hf p ⊆ {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]

Premises used: compl_compl, setOf, Set.compl_subset_compl, aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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}ᶜ

Tactic:
Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)

Premises used: Iff.mpr, Set.Subset.trans, MeasureTheory.subset_toMeasurable, Set.compl_subset_compl
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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
refine :
  Subset.{u_2} (α := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}
    {x : α | p x fun (n : ι) ↦ f n x}
⊢ {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}ᶜ

Tactic:
refine Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)

Premises used: Iff.mpr, Set.Subset.trans, MeasureTheory.subset_toMeasurable, Set.compl_subset_compl
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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
⊢ Subset.{u_2} (α := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}
    {x : α | p x fun (n : ι) ↦ f n x}

Tactic:
fun x hx => hx.2

Premises used: Set.Mem, setOf, Set.Subset, And.right
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
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
⊢ Subset.{u_2} (α := Set α) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}
    {x : α | p x fun (n : ι) ↦ f n x}

Tactic:
exact fun x hx => hx.2