[GOAL]
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ boolIndicator s x = true
[PROOFSTEP]
unfold boolIndicator
[GOAL]
α : Type u_1
s : Set α
x : α
⊢ x ∈ s ↔ (if x ∈ s then true else false) = true
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ x ∈ s ↔ true = true
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ x ∈ s ↔ False
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ boolIndicator s x = false
[PROOFSTEP]
unfold boolIndicator
[GOAL]
α : Type u_1
s : Set α
x : α
⊢ ¬x ∈ s ↔ (if x ∈ s then true else false) = false
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
s : Set α
x : α
h : x ∈ s
⊢ ¬x ∈ s ↔ False
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
s : Set α
x : α
h : ¬x ∈ s
⊢ ¬x ∈ s ↔ false = false
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
s : Set α
t : Set Bool
⊢ boolIndicator s ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ x ∈ boolIndicator s ⁻¹' t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
[PROOFSTEP]
simp only [boolIndicator, mem_preimage]
[GOAL]
case h
α : Type u_1
s : Set α
t : Set Bool
x : α
⊢ (if x ∈ s then true else false) ∈ t ↔ x ∈ (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ s ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ true ∈ t ↔ x ∈ ∅ ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ s ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ sᶜ
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
x : α
h✝² : ¬x ∈ s
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ false ∈ t ↔ x ∈ ∅ ∪ ∅
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
s : Set α
t : Set Bool
⊢ boolIndicator s ⁻¹' t = univ ∨ boolIndicator s ⁻¹' t = s ∨ boolIndicator s ⁻¹' t = sᶜ ∨ boolIndicator s ⁻¹' t = ∅
[PROOFSTEP]
simp only [preimage_boolIndicator_eq_union]
[GOAL]
α : Type u_1
s : Set α
t : Set Bool
⊢ ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = univ ∨
    ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = s ∨
      ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = sᶜ ∨
        ((if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅) = ∅
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : false ∈ t
⊢ s ∪ sᶜ = univ ∨ s ∪ sᶜ = s ∨ s ∪ sᶜ = sᶜ ∨ s ∪ sᶜ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : true ∈ t
h✝ : ¬false ∈ t
⊢ s ∪ ∅ = univ ∨ s ∪ ∅ = s ∨ s ∪ ∅ = sᶜ ∨ s ∪ ∅ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
[GOAL]
case pos
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : false ∈ t
⊢ ∅ ∪ sᶜ = univ ∨ ∅ ∪ sᶜ = s ∨ ∅ ∪ sᶜ = sᶜ ∨ ∅ ∪ sᶜ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
[GOAL]
case neg
α : Type u_1
s : Set α
t : Set Bool
h✝¹ : ¬true ∈ t
h✝ : ¬false ∈ t
⊢ ∅ ∪ ∅ = univ ∨ ∅ ∪ ∅ = s ∨ ∅ ∪ ∅ = sᶜ ∨ ∅ ∪ ∅ = ∅
[PROOFSTEP]
simp [s.union_compl_self]
