awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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
⊢ y ∈ A n
have pos : ∀ (hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal))
  (hsome :
    sorry.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: split_ifs at hsome with hμAn
Cleared hypotheses: hsome
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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
⊢ y ∈ A n
have neg : ∀ (hμAn : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal))
  (hsome :
    sorry.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: split_ifs at hsome with hμAn
Cleared hypotheses: hsome
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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₀ : α), μ = Measure.dirac x₀
have obtain : ∀ (x₀ : α) (hx₀ : Eq (α := Set α) (⋂ (n : ℕ), B n) {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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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₀}
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀
have h : μ = Measure.dirac x₀
Tactic: use x₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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₀}
⊢ μ = Measure.dirac x₀
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
have pos : ∀ (h : x₀ ∈ s),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
Tactic: by_cases h : x₀ ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
have neg : ∀ (h : x₀ ∉ s),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
Tactic: by_cases h : x₀ ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
have pos : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
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
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
have this₁ : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) {x₀} : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
Tactic: have : μ {x₀} ≤ μ s := measure_mono (μ := μ) (by grind)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
have this₁ : LE.le (α := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
Tactic: rw [← hx₀, hBn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
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
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
    (((Measure.dirac x₀ : Measure α) : (a : Set α) → ENNReal) s : ENNReal)
have neg : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
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
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
have this₁ : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) {x₀}ᶜ : ENNReal)
Tactic: have : μ s ≤ μ {x₀}ᶜ := measure_mono (μ := μ) (by grind)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
have this₁ : (μ : (a : Set α) → ENNReal) s ≤ HSub.hSub (α := ENNReal) 1 1
Tactic: rw [← hx₀, measure_compl mBn (by simp), MeasureTheory.measure_univ, hBn] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (a : α) in s, f a ∂μ
have apply : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (a : α) in s, f a ∂μ
Tactic: apply le_antisymm ?_ (withDensity_apply_le f s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
have e_μ : μ.restrict t = μ.restrict s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ (μ.withDensity f : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (a : α) in s, f a ∂μ
have f₁ : ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ
Tactic: calc
  μ.withDensity f s ≤ μ.withDensity f t := measure_mono (subset_toMeasurable μ s)
  _ = ∫⁻ a in t, f a ∂μ := withDensity_apply f (measurableSet_toMeasurable μ s)
  _ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sFinite s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ Eq (α := Measure α) (withDensity 0 f) 0
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((withDensity 0 f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((withDensity 0 f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (a : α) in s, f a ∂0 = ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s
Tactic: rw [withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ μ.withDensity f = μ.withDensity g
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine Measure.ext fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
Tactic: rw [withDensity_apply _ hs, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
⊢ μ.withDensity f ≤ μ.withDensity g
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  LE.le (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_iff.2 fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: rw [withDensity_apply _ hs, withDensity_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have refine : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
Tactic: refine setLIntegral_mono_ae' hs ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ s → f x ≤ g x) x} x}
    a
Tactic: filter_upwards [hfg] with x h_le using fun _ ↦ h_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ s → f x ≤ g x) x} x}
      a
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
have h₁ : ∀ (a : α), f a ≤ g a → a ∈ s → f a ≤ g a
Tactic: filter_upwards [hfg] with x h_le using fun _ ↦ h_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ.withDensity (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f + μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine Measure.ext fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f + μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ
Tactic: rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
    ← lintegral_add_left hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ (μ + ν).withDensity f = μ.withDensity f + ν.withDensity f
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((μ + ν).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.withDensity f + ν.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
⊢ (sum μ).withDensity f = sum fun (n : ι) ↦ (μ n).withDensity f
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ (μ n).withDensity f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ (μ n).withDensity f : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((sum μ).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (∑' (i : ι), ((μ i).withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]