case inl
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
⊢ filter (Eq b) s = {b}

case inr
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
⊢ filter (Eq b) s = ∅
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (Eq b) s = if b ∈ s then {b} else ∅
split_ifs with h
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ {b}
case inl
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
⊢ filter (Eq b) s = {b}
ext
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ s ∧ b = a✝ ↔ a✝ = b
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ {b}
simp only [mem_filter, mem_singleton, decide_eq_true_eq]
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ = b → a✝ ∈ s ∧ b = a✝
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ s ∧ b = a✝ ↔ a✝ = b
refine ⟨fun h => h.2.symm, ?_⟩
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
a✝ : β
h : a✝ ∈ s
⊢ a✝ ∈ s ∧ a✝ = a✝
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ = b → a✝ ∈ s ∧ b = a✝
rintro rfl
no goals
case inl.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
a✝ : β
h : a✝ ∈ s
⊢ a✝ ∈ s ∧ a✝ = a✝
exact ⟨h, rfl⟩
case inr.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ ∅
case inr
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
⊢ filter (Eq b) s = ∅
ext
case inr.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
a✝ : β
⊢ a✝ ∈ s → ¬b = a✝
case inr.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ ∅
simp only [mem_filter, not_and, iff_false_iff, not_mem_empty, decide_eq_true_eq]
case inr.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
m : b ∈ s
⊢ False
case inr.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
a✝ : β
⊢ a✝ ∈ s → ¬b = a✝
rintro m rfl
no goals
case inr.a
α : Type ?u.409796
β : Type u_1
γ : Type ?u.409802
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
m : b ∈ s
⊢ False
exact h m