awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
h : neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
pos :
  ∀ (hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal))
    (hsome :
      ⋯.some (s :=
          ⋂ (n : ℕ),
            if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
        A n),
    y ∈ A n
neg :
  ∀ (hμAn : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal))
    (hsome :
      ⋯.some (s :=
          ⋂ (n : ℕ),
            if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
        (A n)ᶜ),
    y ∈ A n
⊢ y ∈ A n

Tactic:
split_ifs at hsome with hμAn
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
h : neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    A n
⊢ y ∈ A n

Tactic:
simpa [hμAn] using hy
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
h : neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
hμAn : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    (A n)ᶜ
⊢ y ∈ A n

Tactic:
contradiction
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
obtain : ∀ (x₀ : α) (hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}), ∃ (x₀ : α), μ = Measure.dirac x₀
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀

Tactic:
obtain ⟨x₀, hx₀⟩ : ∃ x₀, ⋂ n, B n = {x₀} := by
    simp_rw [eq_singleton_iff_unique_mem]
    have neBn : (⋂ n, B n).Nonempty := by
      by_contra! h
      rw [h] at hBn
      simp_all
    refine ⟨neBn.some, neBn.some_mem, fun y hy ↦ ?_⟩
    refine hAsep y (by trivial) neBn.some (by trivial) fun n ↦ ?_
    have hsome := neBn.some_mem
    simp only [dite_eq_ite, mem_iInter, B] at hsome hy
    specialize hsome n
    specialize hy n
    constructor
    · intro h
      split_ifs at hy with hμAn
      · simpa [hμAn] using hsome
      · contradiction
    · intro h
      split_ifs at hsome with hμAn
      · simpa [hμAn] using hy
      · contradiction
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
h : μ = Measure.dirac x₀
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀

Tactic:
use x₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
⊢ μ = Measure.dirac x₀

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
pos :
  ∀ (h : x₀ ∈ s),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
neg :
  ∀ (h : x₀ ∉ s),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
by_cases h : x₀ ∈ s
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∈ s
pos : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∈ s
⊢ {x₀} ⊆ s

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∈ s
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x₀} : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
have : μ {x₀} ≤ μ s := measure_mono (μ := μ) (by grind)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this_1 : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∈ s
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x₀} : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ LE.le (α := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
rw [← hx₀, hBn] at this
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this_1 : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∈ s
this : LE.le (α := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
neg : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
⊢ s ⊆ {x₀}ᶜ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) {x₀}ᶜ : ENNReal)

Tactic:
have : μ s ≤ μ {x₀}ᶜ := measure_mono (μ := μ) (by grind)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this_1 : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
this :
  LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n)ᶜ : ENNReal)
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this_1 : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) {x₀}ᶜ : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) s ≤ HSub.hSub (α := ENNReal) 1 1

Tactic:
rw [← hx₀, measure_compl mBn (by simp), MeasureTheory.measure_univ, hBn] at this

Premises used: MeasureTheory.measure_compl, MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this_1 : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
x₀ : α
hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
s : Set α
hs : MeasurableSet s
h : x₀ ∉ s
this : (μ : (a : Set α) → ENNReal) s ≤ HSub.hSub (α := ENNReal) 1 1
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ_1 : Measure α
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) ((fun (s : Set α) (x : MeasurableSet s) ↦ ∫⁻ (a : α) in s, f a ∂μ) ∅ ⋯) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
Measure.ofMeasurable_apply s hs

Premises used: MeasureTheory.Measure.ofMeasurable_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in t, f a ∂μ

Tactic:
lintegral_mono_set (subset_toMeasurable (withDensity μ f) s)

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.subset_toMeasurable, MeasureTheory.lintegral_mono_set
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ ∫⁻ (a : α) in t, f a ∂μ = (μ.withDensity f : (a : Set α) → ℝ≥0∞) t

Tactic:
(withDensity_apply f (measurableSet_toMeasurable (withDensity μ f) s)).symm

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.measurableSet_toMeasurable, Eq.symm, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_toMeasurable s

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable (μ.withDensity f) s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s

Tactic:
calc
  ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in t, f a ∂μ :=
    lintegral_mono_set (subset_toMeasurable (withDensity μ f) s)
  _ = μ.withDensity f t :=
    (withDensity_apply f (measurableSet_toMeasurable (withDensity μ f) s)).symm
  _ = μ.withDensity f s := measure_toMeasurable s

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.lintegral_mono_set, Eq.symm, DFunLike.coe, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
apply : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (a : α) in s, f a ∂μ
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
apply le_antisymm ?_ (withDensity_apply_le f s)

Premises used: MeasureTheory.withDensity_apply_le, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_mono (subset_toMeasurable μ s)

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) t = ∫⁻ (a : α) in t, f a ∂μ

Tactic:
withDensity_apply f (measurableSet_toMeasurable μ s)

Premises used: MeasureTheory.measurableSet_toMeasurable, MeasureTheory.withDensity_apply
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
e_μ : μ.restrict t = μ.restrict s
⊢ ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.WithDensity
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ μ.restrict t = μ.restrict s

Tactic:
restrict_toMeasurable_of_sFinite s

Premises used: MeasureTheory.Measure.restrict_toMeasurable_of_sFinite