awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
⊢ ∀ᵐ (x : α) ∂μ, x ∉ t
have this₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have : μ t = 0 := le_antisymm μt bot_le
-- 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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ x ∉ t) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : {x : α | (fun (x : α) ↦ x ∉ t) x}ᶜ = t
Tactic: convert! this
-- 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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ {x : α | (fun (x : α) ↦ x ∉ t) x}ᶜ = t
have h₁ : ∀ (y : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∉ t) x}ᶜ y ↔ y ∈ t
Tactic: ext y
-- 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∞)
⊢ ∀ᵐ (x : α) ∂μ, f x = f' x
have this₁ : ∀ᵐ (x : α) ∂μ, x ∉ t
Tactic: 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]
-- 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 : α) ∂μ, f x = f' x
have h₁ : ∀ (x : α) (hx : x ∉ t), f x = f' x
Tactic: filter_upwards [this] with x hx
-- 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
⊢ f x = f' x
have apply : ∀ (i : (↑s : Type u_2)),
  f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
Tactic: apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
-- 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
apply :
  ∀ (i : (↑s : Type u_2)),
    f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
⊢ f x = f' x
have apply₁ : ∀ (w : β),
  f x < w →
    ∃ (i : (↑s : Type u_2)),
      (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x < w
Tactic: apply (iInf_eq_of_forall_ge_of_forall_gt_exists_lt _ _).symm
-- 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
i : (↑s : Type u_2)
⊢ f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
have pos : ∀ (H : x ∈ u' (↑i : β)),
  f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
Tactic: by_cases H : x ∈ u' i
-- 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
i : (↑s : Type u_2)
pos :
  ∀ (H : x ∈ u' (↑i : β)),
    f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
⊢ f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
have neg : ∀ (H : x ∉ u' (↑i : β)),
  f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
Tactic: by_cases H : x ∈ u' i
-- 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
i : (↑s : Type u_2)
H : x ∈ u' (↑i : β)
⊢ f x ≤ (u' (↑i : β)).piecewise (β := fun (x : α) ↦ β) (fun (x : α) ↦ (↑i : β)) (fun (x : α) ↦ ⊤) x
have pos : f x ≤ (↑i : β)
Tactic: simp only [H, piecewise_eq_of_mem]
-- 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
i : (↑s : Type u_2)
H : x ∈ u' (↑i : β)
⊢ f x ≤ (↑i : β)
have pos : ∀ (hx : (↑i : β) < f x), x ∈ t
Tactic: contrapose! hx
Cleared hypotheses: hx
-- 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
⊢ x ∈ t
have pos : ∀ (r : β) (rs : r ∈ s) (xr : (↑i : β) < r) (rq : r < f x), x ∈ t
Tactic: 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)
-- 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 : α
i : (↑s : Type u_2)
H : x ∈ u' (↑i : β)
hx : (↑i : β) < f x
r : β
rs : r ∈ s
xr : (↑i : β) < r
rq : r < f x
⊢ x ∈ t
have A : x ∈ v (↑i : β) r
Tactic: have A : x ∈ v i r := (huv i r).2.2.2.1 rq
-- 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
⊢ x ∈ t
have pos : Membership.mem (γ := Set α) (⋃ (q : (↑(s ∩ Ioi (↑i : β)) : Type u_2)), u' (↑i : β) ∩ v (↑i : β) (↑q : β)) x
Tactic: refine mem_iUnion.2 ⟨i, ?_⟩