awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set (Set (α × β)))
    (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
    Set.univ

Tactic:
exact ⟨Set.univ, .univ, Set.univ, .univ, Set.univ_prod_univ⟩
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s_1 : Set (α × β)
hs_1 : MeasurableSet s_1
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t
⊢ ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t, f x ∂μ =
    ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t, g x ∂μ

Tactic:
h hs ht
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s_1 : Set (α × β)
hs_1 : MeasurableSet s_1
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t
⊢ ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t, f x ∂μ =
    ∫⁻ (x : α × β) in (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t, g x ∂μ

Tactic:
exact h hs ht
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᶠ[ae μ] g

Tactic:
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
refine :
  ∀ (s : Set α) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᶠ[ae μ] g

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
rw₁ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

Premises used: MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᶠ[ae μ] g

Tactic:
AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_

Premises used: MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
refine_1 : ∫⁻ (x : α), g x ∂μ ≠ ∞
refine_2 :
  ∀ (s : Set α) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᶠ[ae μ] g

Tactic:
refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_

Premises used: MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
refine_1 : ∫⁻ (x : α) in Set.univ, g x ∂μ ≠ ∞
refine_1₁ : Ne (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1₂ : Ne (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1₃ : ∫⁻ (a : α) in Set.univ, f a ∂μ ≠ ∞
refine_1₄ refine_1₅ refine_1₆ refine_1₇ : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α), g x ∂μ ≠ ∞

Tactic:
rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
        withDensity_apply f MeasurableSet.univ, setLIntegral_univ]

Premises used: MeasurableSet.univ, MeasureTheory.withDensity_apply, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
refine_2₁ :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
refine_2₂ refine_2₃ :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

Premises used: MeasureTheory.withDensity_apply
-- 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∞)
haveI : ∀ (this : Encodable (↑s : Type u_2)), AEMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
haveI : Encodable s := s_count.toEncodable
-- 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)
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∞))
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∞))
⊢ ∃ (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
-- 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)
p q : β
H : p ∈ s ∧ q ∈ s ∧ p < q
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∞))
⊢ ∃ (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μ⟩

Premises used: And.right, And.left
-- 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)
p q : β
H : p ∈ s ∧ q ∈ s ∧ p < q
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:
⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩

Premises used: 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)
p q : β
H : p ∈ s ∧ q ∈ s ∧ p < q
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:
exact ⟨u, v, hu, hv, h'u, h'v, fun _ _ _ => hμ⟩
-- 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)
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∞))

Tactic:
⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩

Premises used: Set.subset_univ, Set.univ, And.intro, Exists.intro, MeasurableSet.univ
-- 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)
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
neg :
  ∀ (ps : p ∈ s) (qs : q ∈ s) (pq : p < q), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ univ) : ℝ≥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:
refine
        ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩
-- 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)
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
ps : p ∈ s
qs : q ∈ s
pq : p < q
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(H ⟨ps, qs, pq⟩).elim

Premises used: False.elim, And.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)
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
ps : p ∈ s
qs : q ∈ s
pq : p < q
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ univ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (H ⟨ps, qs, pq⟩).elim

Premises used: False.elim, And.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)
⊢ ∀ (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
-- 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)
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∞))
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 μ
⊢ AEMeasurable f μ

Tactic:
choose! u v huv using h'
-- 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
i : β
⊢ MeasurableSet (u' i)

Tactic:
MeasurableSet.biInter (s_count.mono inter_subset_left) fun b _ => (huv i b).1

Premises used: Set.inter_subset_left, And.left, MeasurableSet.biInter, Set.Countable.mono
-- 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
i : β
⊢ MeasurableSet (u' i)

Tactic:
exact MeasurableSet.biInter (s_count.mono inter_subset_left) fun b _ => (huv i b).1

Premises used: Set.inter_subset_left, And.left, MeasurableSet.biInter, Set.Countable.mono
-- 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
⊢ ∀ (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