awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    MeasurableSet (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s))
pos₁ :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    MeasurableSet
      (h's.choose (p := fun (t : Set α) ↦
        t ⊇ s ∧
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)))
neg :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ¬∃ t ⊇ s,
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    MeasurableSet
      (⋯.choose (p := fun (t : Set α) ↦
        s ⊆ t ∧
          MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
⊢ MeasurableSet.{u_1} (α := α)
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
split_ifs with hs h's
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ MeasurableSet (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s))

Tactic:
hs.choose_spec.2.1

Premises used: Exists.choose_spec, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ∃ t ⊇ s,
    MeasurableSet t ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ MeasurableSet
    (h's.choose (p := fun (t : Set α) ↦
      t ⊇ s ∧
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)))

Tactic:
h's.choose_spec.2.1

Premises used: Exists.choose_spec, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ¬∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ MeasurableSet
    (⋯.choose (p := fun (t : Set α) ↦
      s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))

Tactic:
(exists_measurable_superset μ s).choose_spec.2.1

Premises used: Exists.choose_spec, And.right, And.left, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ MeasurableSet (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s))

Tactic:
exacts [hs.choose_spec.2.1, h's.choose_spec.2.1,
          (exists_measurable_superset μ s).choose_spec.2.1]

Premises used: Exists.choose_spec, And.right, And.left, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
          h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
        else
          if h' :
              ∃ t ⊇ s,
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
            h'.choose (p := fun (t : Set α) ↦
              t ⊇ s ∧
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
          else
            ⋯.choose (p := fun (t : Set α) ↦
              s ⊆ t ∧
                MeasurableSet t ∧
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [toMeasurable_def]

Premises used: MeasureTheory.toMeasurable_def
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (h's.choose (p := fun (t : Set α) ↦
            t ⊇ s ∧
              MeasurableSet t ∧
                ∀ (u : Set α),
                  MeasurableSet u →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
neg :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ¬∃ t ⊇ s,
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (⋯.choose (p := fun (t : Set α) ↦
            s ⊆ t ∧
              MeasurableSet t ∧
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
          h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
        else
          if h' :
              ∃ t ⊇ s,
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
            h'.choose (p := fun (t : Set α) ↦
              t ⊇ s ∧
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
          else
            ⋯.choose (p := fun (t : Set α) ↦
              s ⊆ t ∧
                MeasurableSet t ∧
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
split_ifs with hs h's
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_congr hs.choose_spec.2.2

Premises used: MeasureTheory.measure_congr, Exists.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact measure_congr hs.choose_spec.2.2

Premises used: MeasureTheory.measure_congr, Exists.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ∃ t ⊇ s,
    MeasurableSet t ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (h's.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa only [inter_univ] using h's.choose_spec.2.2 univ MeasurableSet.univ

Premises used: Exists.choose_spec, Set.univ, Set.inter_univ, And.right, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ¬∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(exists_measurable_superset μ s).choose_spec.2.2

Premises used: Exists.choose_spec, And.right, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
h's :
  ¬∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact (exists_measurable_superset μ s).choose_spec.2.2

Premises used: Exists.choose_spec, And.right, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : Measurable f
⊢ AEMeasurable f μ

Tactic:
⟨f, h, ae_eq_refl f⟩

Premises used: AEMeasurable, MeasureTheory.ae_eq_refl, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
inst_1 : DiscreteMeasurableSpace α
⊢ AEMeasurable f μ

Tactic:
Measurable.of_discrete.aemeasurable

Premises used: Measurable.aemeasurable, Measurable.of_discrete
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
⊢ Measurable (mk f h)

Tactic:
(Classical.choose_spec h).1

Premises used: AEMeasurable.mk, Classical.choose_spec, And.left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
f : α → β
μ : Measure α
h : AEMeasurable f μ
⊢ f =ᶠ[ae μ] mk f h

Tactic:
(Classical.choose_spec h).2

Premises used: AEMeasurable.mk, Classical.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
f g : α → β
μ : Measure α
hf : AEMeasurable f μ
h : f =ᶠ[ae μ] g
⊢ AEMeasurable g μ

Tactic:
⟨hf.mk f, hf.measurable_mk, h.symm.trans hf.ae_eq_mk⟩

Premises used: Filter.EventuallyEq.trans, AEMeasurable, AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
f g : α → β
μ : Measure α
h : f =ᶠ[ae μ] g
⊢ AEMeasurable f μ ↔ AEMeasurable g μ

Tactic:
⟨fun hf => AEMeasurable.congr hf h, fun hg => AEMeasurable.congr hg h.symm⟩

Premises used: AEMeasurable.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
b : β
⊢ AEMeasurable.{u_1, u_2} (β := β) (fun (_a : α) ↦ b) μ

Tactic:
measurable_const.aemeasurable

Premises used: Measurable.aemeasurable, measurable_const
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ AEMeasurable id μ

Tactic:
measurable_id.aemeasurable

Premises used: Measurable.aemeasurable, measurable_id
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ AEMeasurable (β := α) (fun (x : α) ↦ x) μ

Tactic:
measurable_id.aemeasurable

Premises used: Measurable.aemeasurable, measurable_id
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : MeasurableSpace δ
f : α → δ
g : δ → β
hg : Measurable g
hf : AEMeasurable f μ
⊢ AEMeasurable (g ∘ f) μ

Tactic:
⟨g ∘ hf.mk f, hg.comp hf.measurable_mk, EventuallyEq.fun_comp hf.ae_eq_mk _⟩

Premises used: AEMeasurable, Measurable.comp, Function.comp, AEMeasurable.mk, And.intro, Exists.intro, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.fun_comp, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
β : Type u_2
δ : Type u_4
m : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : MeasurableSpace δ
f : α → δ
g : δ → β
hg : Measurable g
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ g (f x)) μ

Tactic:
Measurable.comp_aemeasurable hg hf

Premises used: Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
hg : AEMeasurable g μ
a : δ
right : EventuallyEq.{u_1, u_7} (β := X a) (ae μ) (fun (x : α) ↦ g x a) fun (x : α) ↦ mk g hg x a
⊢ AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ

Tactic:
use fun x ↦ hg.mk g x a, hg.measurable_mk.eval

Premises used: AEMeasurable.mk, Measurable.eval, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
hg : AEMeasurable g μ
a : δ
⊢ EventuallyEq.{u_1, u_7} (β := X a) (ae μ) (fun (x : α) ↦ g x a) fun (x : α) ↦ mk g hg x a

Tactic:
hg.ae_eq_mk.mono fun _ h ↦ congrFun h _

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, congrFun, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
hg : AEMeasurable g μ
a : δ
⊢ EventuallyEq.{u_1, u_7} (β := X a) (ae μ) (fun (x : α) ↦ g x a) fun (x : α) ↦ mk g hg x a

Tactic:
exact hg.ae_eq_mk.mono fun _ h ↦ congrFun h _

Premises used: Filter.Eventually.mono, congrFun, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
mp : AEMeasurable g μ → ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
mpr : (∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ) → AEMeasurable g μ
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ

Tactic:
AEMeasurable.eval

Premises used: AEMeasurable.eval
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ → ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ

Tactic:
exact AEMeasurable.eval

Premises used: AEMeasurable.eval
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
h : ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
right : g =ᶠ[ae μ] fun (x : α) (a : δ) ↦ AEMeasurable.mk (fun (x : α) ↦ g x a) ⋯ x
⊢ AEMeasurable g μ

Tactic:
use fun x a ↦ (h a).mk _ x, measurable_pi_lambda _ fun a ↦ (h a).measurable_mk

Premises used: measurable_pi_lambda, AEMeasurable.mk, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
h : ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
⊢ g =ᶠ[ae μ] fun (x : α) (a : δ) ↦ AEMeasurable.mk (fun (x : α) ↦ g x a) ⋯ x

Tactic:
(eventually_countable_forall.mpr fun a ↦ (h a).ae_eq_mk).mono fun _ h ↦ funext h

Premises used: Iff.mpr, Filter.EventuallyEq, Filter.Eventually.mono, funext, AEMeasurable.ae_eq_mk, eventually_countable_forall
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
h : ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
⊢ g =ᶠ[ae μ] fun (x : α) (a : δ) ↦ AEMeasurable.mk (fun (x : α) ↦ g x a) ⋯ x

Tactic:
exact (eventually_countable_forall.mpr fun a ↦ (h a).ae_eq_mk).mono fun _ h ↦ funext h

Premises used: Iff.mpr, Filter.Eventually.mono, funext, AEMeasurable.ae_eq_mk, eventually_countable_forall
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
f : α → (a : δ) → X a
hf : ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (c : α) ↦ f c a) μ
⊢ AEMeasurable f μ

Tactic:
aemeasurable_pi_iff.mpr hf

Premises used: Iff.mpr, aemeasurable_pi_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ∀ (x : MeasuredSets μ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((↑x : Set α) ∆ (↑x : Set α)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ ∀ (x y : MeasuredSets μ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((↑x : Set α) ∆ (↑y : Set α)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) ((↑y : Set α) ∆ (↑x : Set α)) : ℝ≥0∞)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
⊢ edist s t = (μ : (a : Set α) → ℝ≥0∞) ((↑s : Set α) ∆ (↑t : Set α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) ≤
    edist s t

Tactic:
le_measure_diff.trans <| measure_mono subset_union_left

Premises used: Set.subset_union_left, MeasureTheory.measure_mono, LE.le.trans, MeasureTheory.le_measure_diff
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ Continuous (Y := ℝ≥0∞) fun (s : MeasuredSets μ) ↦ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)

Tactic:
continuous_of_le_add_edist 1 ENNReal.one_ne_top fun s t ↦ ?_

Premises used: continuous_of_le_add_edist, OfNat.ofNat, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
refine :
  ∀ (s t : MeasuredSets μ),
    (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) (1 * edist s t)
⊢ Continuous (Y := ℝ≥0∞) fun (s : MeasuredSets μ) ↦ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)

Tactic:
refine continuous_of_le_add_edist 1 ENNReal.one_ne_top fun s t ↦ ?_

Premises used: continuous_of_le_add_edist, OfNat.ofNat, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) ≤
    edist s t
⊢ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) (1 * edist s t)

Tactic:
rw [one_mul, ← tsub_le_iff_left]

Premises used: tsub_le_iff_left, one_mul
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) ≤
    edist s t

Tactic:
sub_le_edist s t

Premises used: MeasureTheory.MeasuredSets.sub_le_edist
-- Module: Mathlib.MeasureTheory.Measure.MeasuredSets
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) ≤
    edist s t

Tactic:
exact sub_le_edist s t

Premises used: MeasureTheory.MeasuredSets.sub_le_edist