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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)

Tactic:
have hBn : μ (⋂ n, B n) = 1 := by
    refine (prob_compl_eq_zero_iff mBn).mp ?_
    simp only [dite_eq_ite, compl_iInter, measure_iUnion_null_iff, B]
    intro n
    split_ifs with h
    · simp_all
    · rw [compl_compl]
      rcases μ.zero_one (A n) with (h₀ | h₁)
      · exact h₀
      · 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)
simp_rw :
  ∃ (x₀ : α),
    Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x₀ ∧ ∀ (x : α), Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x → x = x₀
⊢ ∃ (x₀ : α), Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}

Tactic:
simp_rw [eq_singleton_iff_unique_mem]

Premises used: Set.eq_singleton_iff_unique_mem
-- 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)
by_contra! : ∀ (h : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅), False
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)

Tactic:
by_contra! 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)
h : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) ∅ : ENNReal) (1 : ENNReal)

Tactic:
rw [h] at hBn
-- 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)
h : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅
hBn₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) ∅ : ENNReal) (1 : ENNReal)
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅

Tactic:
rw [h] at hBn
-- 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) ∅ : ENNReal) (1 : ENNReal)
h : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅
⊢ False

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)
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)

Tactic:
have neBn : (⋂ n, B n).Nonempty := by
      by_contra! h
      rw [h] at hBn
      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)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
⊢ ∃ (x₀ : α),
    Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x₀ ∧ ∀ (x : α), Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x → x = x₀

Tactic:
⟨neBn.some, neBn.some_mem, fun y hy ↦ ?_⟩

Premises used: Set.Nonempty.some_mem, And.intro, Exists.intro, Set.Nonempty.some
-- 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)
refine : ∀ (y : α) (hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y), y = neBn.some (s := ⋂ (n : ℕ), B n)
⊢ ∃ (x₀ : α),
    Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x₀ ∧ ∀ (x : α), Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x → x = x₀

Tactic:
refine ⟨neBn.some, neBn.some_mem, fun y 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 : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
⊢ Membership.mem (γ := Set α) univ y

Tactic:
trivial
-- 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 : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
⊢ Membership.mem (γ := Set α) univ (neBn.some (s := ⋂ (n : ℕ), B n))

Tactic:
trivial
-- 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 : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
refine : ∀ (n : ℕ), y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
⊢ y = neBn.some (s := ⋂ (n : ℕ), B n)

Tactic:
refine hAsep y (by trivial) neBn.some (by trivial) fun n ↦ ?_

Premises used: Set.Nonempty.some
-- 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 : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
n : ℕ
⊢ Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) (neBn.some (s := ⋂ (n : ℕ), B n))

Tactic:
have hsome := neBn.some_mem
-- 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 : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
n : ℕ
hsome : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) (neBn.some (s := ⋂ (n : ℕ), B n))
⊢ ∀ (i : ℕ),
    ⋯.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 i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ

Tactic:
simp only [dite_eq_ite, mem_iInter, B] at hsome hy

Premises used: Set.mem_iInter, 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)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
n : ℕ
hsome : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) (neBn.some (s := ⋂ (n : ℕ), B n))
hsome₁ :
  ∀ (i : ℕ),
    ⋯.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 i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
⊢ ∀ (i : ℕ), y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ

Tactic:
simp only [dite_eq_ite, mem_iInter, B] at hsome hy

Premises used: Set.mem_iInter, 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)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ∀ (i : ℕ),
    ⋯.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 i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
hy :
  ∀ (i : ℕ), y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
⊢ ⋯.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)ᶜ

Tactic:
specialize hsome 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)ᶜ
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 :
  ∀ (i : ℕ), y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
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)ᶜ
⊢ y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ

Tactic:
specialize hy 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)ᶜ
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)ᶜ
mp : y ∈ A n → neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
mpr : neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n → y ∈ A n
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n

Tactic:
constructor
-- 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 : y ∈ A n
pos :
  ∀ (hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)) (hy : y ∈ A n),
    neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
neg :
  ∀ (hμAn : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)) (hy : y ∈ (A n)ᶜ),
    neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
⊢ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n

Tactic:
split_ifs at hy 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 : ℕ
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)ᶜ
h : y ∈ A n
hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
hy : y ∈ A n
⊢ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n

Tactic:
simpa [hμAn] using hsome
-- 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)ᶜ
h : y ∈ A n
hμAn : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
hy : y ∈ (A n)ᶜ
⊢ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n

Tactic:
contradiction