α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ a ∈ ↑(ofSet s) b ↔ a = b ∧ a ∈ s
dsimp [ofSet]
case inl
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a ∈ some b ↔ a = b ∧ a ∈ s

case inr
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : ¬b ∈ s
⊢ a ∈ none ↔ a = b ∧ a ∈ s
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
⊢ (a ∈ if b ∈ s then some b else none) ↔ a = b ∧ a ∈ s
split_ifs with h
case inl
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a = b → a ∈ s
case inl
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a ∈ some b ↔ a = b ∧ a ∈ s
simp only [mem_def, eq_comm, some.injEq, iff_self_and]
case inl
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∈ s
⊢ a ∈ s
case inl
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : b ∈ s
⊢ a = b → a ∈ s
rintro rfl
no goals
case inl
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : a ∈ s
⊢ a ∈ s
exact h
case inr
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : ¬b ∈ s
⊢ a = b → ¬a ∈ s
case inr
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : ¬b ∈ s
⊢ a ∈ none ↔ a = b ∧ a ∈ s
simp only [mem_def, false_iff, not_and]
case inr
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : ¬a ∈ s
⊢ ¬a ∈ s
case inr
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a b : α
h : ¬b ∈ s
⊢ a = b → ¬a ∈ s
rintro rfl
no goals
case inr
α : Type u
β : Type v
γ : Type w
δ : Type x
s✝ : Set α
inst✝¹ : DecidablePred fun x => x ∈ s✝
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
a : α
h : ¬a ∈ s
⊢ ¬a ∈ s
exact h