-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_generateFrom_singleton_iff {s t : Set α} :
    MeasurableSet[MeasurableSpace.generateFrom {s}] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Proof state:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
⊢ x = {True}

Tactic:
ext p

Result:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
p : Prop
⊢ p ∈ x ↔ p ∈ {True}

Proof state:
case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.Basic._hyg.15042.«1»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : False ∈ x
⊢ False ∈ ∅

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
have hx : x = {False} := by
  ext p
  refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩
  by_contra hpneg
  simp only [eq_iff_iff, iff_false, not_not] at hpneg
  refine hT ?_
  convert hp
  simpa

Result:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
hx : x = {False}
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ x = univ

Tactic:
refine subset_antisymm (subset_univ _) ?_

Result:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ univ ⊆ x

Proof state:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
hx : x = {True}
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
this : x = ∅
⊢ (fun x => x ∈ s) ⁻¹' x ⊆ ∅

Tactic:
simp only [this, preimage_empty, subset_refl]

Result:
no goals

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
hx : x = {False}
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
refine Or.inr <| Or.inr <| Or.inl <| ?_

Result:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
hx : x = {False}
⊢ (fun x => x ∈ s) ⁻¹' x = sᶜ

Proof state:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
hp : p ∈ x
hpneg : ¬p = False
⊢ False

Tactic:
simp only [eq_iff_iff, iff_false, not_not] at hpneg

Result:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
hp : p ∈ x
hpneg : p
⊢ False

Proof state:
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
⊢ x = {False}

Tactic:
ext p

Result:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
⊢ p ∈ x ↔ p ∈ {False}

Proof state:
α : Type u_1
s t : Set α
⊢ t ∈ {t_1 | ∃ s', MeasurableSet s' ∧ (fun x => x ∈ s) ⁻¹' s' = t} ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
simp_rw [MeasurableSpace.measurableSet_top, true_and, mem_setOf_eq]

Result:
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x => x ∈ s) ⁻¹' s' = t) ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Proof state:
case h.e'_5.a
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
hp : p ∈ x
hpneg : p
⊢ True ↔ p

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
⊢ MeasurableSet t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
change t ∈ {t | _} ↔ _

Result:
α : Type u_1
s t : Set α
⊢ t ∈ {t_1 | ∃ s', MeasurableSet s' ∧ (fun x => x ∈ s) ⁻¹' s' = t} ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
hx : x = {False}
⊢ {a | a ∉ s} = sᶜ

Tactic:
rfl

Result:
no goals

Proof state:
case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = sᶜ

Tactic:
use {False}

Result:
case h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' {False} = sᶜ

Proof state:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
p : Prop
hp : p ∈ x
⊢ p = True

Tactic:
by_contra hpneg

Result:
case h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∉ x
p : Prop
hp : p ∈ x
hpneg : ¬p = True
⊢ False

Proof state:
case mpr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = ∅

case mpr.inr.inl
α : Type u_1
t : Set α
⊢ ∃ s', (fun x => x ∈ t) ⁻¹' s' = t

case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = sᶜ

case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = univ

Tactic:
on_goal 1 => use ∅

Result:
case h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' ∅ = ∅

case mpr.inr.inl
α : Type u_1
t : Set α
⊢ ∃ s', (fun x => x ∈ t) ⁻¹' s' = t

case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = sᶜ

case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = univ

Proof state:
case h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' ∅ = ∅

case h
α : Type u_1
t : Set α
⊢ (fun x => x ∈ t) ⁻¹' {True} = t

case mpr.inr.inr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = sᶜ

case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = univ

Tactic:
on_goal 3 => use {False}

Result:
case h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' ∅ = ∅

case h
α : Type u_1
t : Set α
⊢ (fun x => x ∈ t) ⁻¹' {True} = t

case h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' {False} = sᶜ

case mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = univ

Proof state:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
p : Prop
hp : p ∈ x
⊢ p ∈ ∅

Tactic:
fin_cases p

Result:
case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.Basic._hyg.15042.«0»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : True ∈ x
⊢ True ∈ ∅

case neg.«_@».Mathlib.MeasureTheory.MeasurableSpace.Basic._hyg.15042.«1»
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
hp : False ∈ x
⊢ False ∈ ∅

Proof state:
case mp
α : Type u_1
s t : Set α
⊢ (∃ s', (fun x => x ∈ s) ⁻¹' s' = t) → t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ

Tactic:
rintro ⟨x, rfl⟩

Result:
case mp.intro
α : Type u_1
s : Set α
x : Set Prop
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Proof state:
case mpr.inr.inl
α : Type u_1
t : Set α
⊢ ∃ s', (fun x => x ∈ t) ⁻¹' s' = t

Tactic:
use {True}

Result:
case h
α : Type u_1
t : Set α
⊢ (fun x => x ∈ t) ⁻¹' {True} = t

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
hx : x = {False}
⊢ (fun x => x ∈ s) ⁻¹' x = sᶜ

Tactic:
simp [hx]

Result:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
hx : x = {False}
⊢ {a | a ∉ s} = sᶜ

Proof state:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
refine Or.inl <| subset_antisymm ?_ <| empty_subset _

Result:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ (fun x => x ∈ s) ⁻¹' x ⊆ ∅

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ (fun x => x ∈ s) ⁻¹' x = ∅ ∨ (fun x => x ∈ s) ⁻¹' x = s ∨ (fun x => x ∈ s) ⁻¹' x = sᶜ ∨ (fun x => x ∈ s) ⁻¹' x = univ

Tactic:
refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_

Result:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ univ ⊆ (fun x => x ∈ s) ⁻¹' x

Proof state:
case mpr.inl
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = ∅

Tactic:
use ∅

Result:
case h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' ∅ = ∅