awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
h_2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h_2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h_2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h_2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h_2 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
inl : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)), IsProbabilityMeasure μ
inr : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)), IsProbabilityMeasure μ
⊢ IsProbabilityMeasure μ

Tactic:
rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with (h | h)

Premises used: MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)
⊢ IsProbabilityMeasure μ

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ IsProbabilityMeasure μ

Tactic:
⟨h⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ IsProbabilityMeasure μ

Tactic:
exact ⟨h⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := by
    rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with (h | h)
    · simp_all
    · exact ⟨h⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
obtain :
  ∀ (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),
    ∃ (x₀ : α), μ = Measure.dirac x₀
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀

Tactic:
obtain ⟨A, hAm, hAsep⟩ := exists_seq_separating (α := α) MeasurableSet.univ univ

Premises used: exists_seq_separating, Set.univ, MeasurableSet.univ
-- 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)ᶜ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)

Tactic:
MeasurableSet.iInter fun n ↦ ?_

Premises used: MeasurableSet.iInter
-- 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)ᶜ
refine : ∀ (n : ℕ), MeasurableSet (B n)
⊢ MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)

Tactic:
refine MeasurableSet.iInter fun n ↦ ?_

Premises used: MeasurableSet.iInter
-- 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)ᶜ
n : ℕ
simp :
  MeasurableSet (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)
⊢ MeasurableSet (B n)

Tactic:
simp only [dite_eq_ite, B]

Premises used: dite_eq_ite
-- 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)ᶜ
n : ℕ
pos : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) → MeasurableSet (A n)
neg : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) → MeasurableSet (A n)ᶜ
⊢ MeasurableSet (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)

Tactic:
split_ifs
-- 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)ᶜ
n : ℕ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ MeasurableSet (A n)

Tactic:
hAm n
-- 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)ᶜ
n : ℕ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ MeasurableSet (A n)

Tactic:
exact hAm n
-- 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)ᶜ
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ MeasurableSet (A n)ᶜ

Tactic:
(hAm n).compl

Premises used: MeasurableSet.compl
-- 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)ᶜ
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ MeasurableSet (A n)ᶜ

Tactic:
exact (hAm n).compl

Premises used: MeasurableSet.compl
-- 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)ᶜ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)

Tactic:
have mBn : MeasurableSet (⋂ n, B n) := by
    refine MeasurableSet.iInter fun n ↦ ?_
    simp only [dite_eq_ite, B]
    split_ifs
    · exact hAm n
    · exact (hAm n).compl
-- 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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)

Tactic:
(prob_compl_eq_zero_iff mBn).mp ?_

Premises used: MeasureTheory.prob_compl_eq_zero_iff, Iff.mp
-- 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)
refine : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n)ᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)

Tactic:
refine (prob_compl_eq_zero_iff mBn).mp ?_

Premises used: MeasureTheory.prob_compl_eq_zero_iff, Iff.mp
-- 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)
simp :
  ∀ (i : ℕ),
    Eq (α := ENNReal)
      ((μ : (a : Set α) → ENNReal)
          (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ)ᶜ :
        ENNReal)
      (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n)ᶜ : ENNReal) (0 : ENNReal)

Tactic:
simp only [dite_eq_ite, compl_iInter, measure_iUnion_null_iff, B]

Premises used: Set.compl_iInter, MeasureTheory.measure_iUnion_null_iff, dite_eq_ite
-- 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)
n : ℕ
pos :
  ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜ : ENNReal) (0 : ENNReal)
neg :
  ∀ (h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal)
        (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)ᶜ :
      ENNReal)
    (0 : ENNReal)

Tactic:
split_ifs with 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)
n : ℕ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜ : ENNReal) (0 : 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)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
neg : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜᶜ : ENNReal) (0 : ENNReal)

Tactic:
rw [compl_compl]

Premises used: compl_compl
-- 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)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
neg :
  ∀ (h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
neg₁ :
  ∀ (h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)

Tactic:
rcases μ.zero_one (A n) with (h₀ | h₁)

Premises used: MeasureTheory.Measure.zero_one
-- 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)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)

Tactic:
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)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)

Tactic:
exact 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)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)

Tactic:
simp_all