-- 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:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ univ ⊆ (fun x => x ∈ s) ⁻¹' x

Tactic:
suffices x = univ by simp only [this, preimage_univ, subset_refl]

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

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

Tactic:
refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩

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

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

Tactic:
simp [compl_def]

Result:
no goals

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 h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' {False} = sᶜ

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

Tactic:
all_goals
  simp [compl_def]

Result:
no goals

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

Tactic:
intro p hp

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

Proof state:
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 ∈ ∅

Tactic:
contradiction

Result:
no goals

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ {True, False} ⊆ x

Tactic:
rintro - (rfl | rfl)

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

case pos.inr
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ False ∈ x

Proof state:
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

Tactic:
by_cases hT : True ∈ x

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

case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
⊢ (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 h
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∈ x
p : Prop
hp : p ∈ x
hpneg : p
⊢ False

Tactic:
refine hT ?_

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 ∈ x

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

Tactic:
constructor

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

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

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

Tactic:
assumption

Result:
no goals

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

Tactic:
refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩

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

Proof state:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ 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:
by_cases hF : False ∈ x

Result:
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

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

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

Tactic:
rw [subset_empty_iff] at this

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

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
⊢ True ∈ x

Tactic:
convert hp

Result:
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

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

Tactic:
rw [univ_eq_true_false]

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

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

Tactic:
assumption

Result:
no goals

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

Tactic:
suffices x ⊆ ∅ by
  rw [subset_empty_iff] at this
  simp only [this, preimage_empty, subset_refl]

Result:
case neg
α : Type u_1
s : Set α
x : Set Prop
hT : True ∉ x
hF : False ∉ x
⊢ x ⊆ ∅

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

Tactic:
simp only [this, preimage_univ, subset_refl]

Result:
no goals

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

Tactic:
rintro (rfl | rfl | rfl | rfl)

Result:
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

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 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

Tactic:
on_goal 4 => use Set.univ

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 h
α : Type u_1
s : Set α
⊢ (fun x => x ∈ s) ⁻¹' univ = univ

Proof state:
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

Tactic:
on_goal 2 => use {True}

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 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 mpr.inr.inr.inr
α : Type u_1
s : Set α
⊢ ∃ s', (fun x => x ∈ s) ⁻¹' s' = univ

Tactic:
use Set.univ

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

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

Tactic:
exact hF (by convert hp)

Result:
no goals