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∞)
⊢ AEMeasurable f μ
have haveI : ∀ (this : Encodable (↑s : Type u_2)), AEMeasurable f μ
Tactic: haveI : Encodable s := s_count.toEncodable
-- 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 : Encodable (↑s : Type u_2)
p q : β
⊢ ∃ (u : Set α) (v : Set α),
    MeasurableSet u ∧
      MeasurableSet v ∧
        {x : α | f x < p} ⊆ u ∧
          {x : α | q < f x} ⊆ v ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
have pos : ∀ (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 ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
-- 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 : Encodable (↑s : Type u_2)
p q : β
pos :
  ∀ (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 ∧
              (p ∈ s → q ∈ s → p < q → 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 ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
have neg : ∀ (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 ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
-- 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 : Encodable (↑s : Type u_2)
p q : β
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 ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
have pos : ∀ (u v : Set α) (hu : MeasurableSet u) (hv : MeasurableSet v) (h'u : {x : α | f x < p} ⊆ u)
  (h'v : {x : α | q < f x} ⊆ v) (hμ : 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 ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
-- 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 : Encodable (↑s : Type u_2)
p q : β
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 ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
have neg : ∀ (ps : p ∈ s) (qs : q ∈ s) (pq : p < q), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine
        ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩
-- 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)
⊢ AEMeasurable f μ
have h' : ∀ (p q : β),
  ∃ (u : Set α) (v : Set α),
    MeasurableSet u ∧
      MeasurableSet v ∧
        {x : α | f x < p} ⊆ u ∧
          {x : α | q < f x} ⊆ v ∧
            (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: have h' : ∀ p q, ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧
      { x | f x < p } ⊆ u ∧ { x | q < f x } ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0) := by
    intro p q
    by_cases H : p ∈ s ∧ q ∈ s ∧ p < q
    · rcases h p H.1 q H.2.1 H.2.2 with ⟨u, v, hu, hv, h'u, h'v, hμ⟩
      exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩
    · refine
        ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩
      exact (H ⟨ps, qs, pq⟩).elim
-- 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 : Encodable (↑s : Type u_2)
h' :
  ∀ (p q : β),
    ∃ (u : Set α) (v : Set α),
      MeasurableSet u ∧
        MeasurableSet v ∧
          {x : α | f x < p} ⊆ u ∧
            {x : α | q < f x} ⊆ v ∧
              (p ∈ s → q ∈ s → p < q → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ v) : ℝ≥0∞) (0 : ℝ≥0∞))
⊢ AEMeasurable f μ
have choose! : ∀ (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∞))),
  AEMeasurable f μ
Tactic: choose! u v huv using h'
Cleared hypotheses: h'
-- 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
⊢ AEMeasurable f μ
have u'_meas : ∀ (i : β), MeasurableSet (u' i)
Tactic: have u'_meas : ∀ i, MeasurableSet (u' i) := by
    intro i
    exact MeasurableSet.biInter (s_count.mono inter_subset_left) fun b _ => (huv i b).1
-- 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 : 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
⊢ Measurable f'
have funProp : ∀ (i : (↑s : Type u_2)), MeasurableSet (u' (↑i : β))
Tactic: fun_prop (disch := simp_all)
-- 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
⊢ AEMeasurable f μ
have f'_meas : Measurable f'
Tactic: have f'_meas : Measurable f' := by fun_prop (disch := simp_all)
-- 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 : 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 : β)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)) (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)),
        (μ : (a : Set α) → ℝ≥0∞) (u' (↑p : β) ∩ v (↑p : β) (↑q : β)) :
      ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞)
  (∑' (i : (↑s : Type u_2)),
    (μ : (a : Set α) → ℝ≥0∞) (⋃ (q : (↑(s ∩ Ioi (↑i : β)) : Type u_2)), u' (↑i : β) ∩ v (↑i : β) (↑q : β)))
  (∑' (p : (↑s : Type u_2)) (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)),
    (μ : (a : Set α) → ℝ≥0∞) (u' (↑p : β) ∩ v (↑p : β) (↑q : β)))
Tactic: refine (measure_iUnion_le _).trans ?_
-- 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 : 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 : β)
⊢ LE.le (α := ℝ≥0∞)
    (∑' (i : (↑s : Type u_2)),
      (μ : (a : Set α) → ℝ≥0∞) (⋃ (q : (↑(s ∩ Ioi (↑i : β)) : Type u_2)), u' (↑i : β) ∩ v (↑i : β) (↑q : β)))
    (∑' (p : (↑s : Type u_2)) (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)),
      (μ : (a : Set α) → ℝ≥0∞) (u' (↑p : β) ∩ v (↑p : β) (↑q : β)))
have refine : ∀ (p : (↑s : Type u_2)),
  LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)) : ℝ≥0∞)
    (∑' (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (u' (↑p : β) ∩ v (↑p : β) (↑q : β)) : ℝ≥0∞)
Tactic: refine ENNReal.tsum_le_tsum fun p => ?_
-- 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 : β)
p : (↑s : Type u_2)
⊢ LE.le (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ∩ v (↑p : β) (↑q : β)) : ℝ≥0∞)
    (∑' (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (u' (↑p : β) ∩ v (↑p : β) (↑q : β)) : ℝ≥0∞)
have this₁ : Countable.{u_2 + 1} (↑(s ∩ Ioi (↑p : β)) : Type u_2)
Tactic: haveI := (s_count.mono (s.inter_subset_left (t := Ioi ↑p))).to_subtype
-- 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 : 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 : β)
⊢ LE.le (α := ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)) (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)),
      (μ : (a : Set α) → ℝ≥0∞) (u' (↑p : β) ∩ v (↑p : β) (↑q : β)))
    (∑' (p : (↑s : Type u_2)) (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)),
      (μ : (a : Set α) → ℝ≥0∞) (u (↑p : β) (↑q : β) ∩ v (↑p : β) (↑q : β)))
have h₁ : ∀ (p : (↑s : Type u_2)) (q : (↑(s ∩ Ioi (↑p : β)) : Type u_2)), u' (↑p : β) ⊆ u (↑p : β) (↑q : β)
Tactic: gcongr with p q
-- 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 : β)
⊢ AEMeasurable f μ
have μt : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have μt : μ t ≤ 0 :=
    calc
      μ t ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u' p ∩ v p q) := by
        refine (measure_iUnion_le _).trans ?_
        refine ENNReal.tsum_le_tsum fun p => ?_
        haveI := (s_count.mono (s.inter_subset_left (t := Ioi ↑p))).to_subtype
        apply measure_iUnion_le
      _ ≤ ∑' (p : s) (q : ↥(s ∩ Ioi p)), μ (u p q ∩ v p q) := by
        gcongr with p q
        exact biInter_subset_of_mem q.2
      _ = ∑' (p : s) (_ : ↥(s ∩ Ioi p)), (0 : ℝ≥0∞) := by grind
      _ = 0 := by simp only [tsum_zero]