no goals
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s
simpa only [Multiset.mem_cons, mem_insert] using h
no goals
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s
simpa only [Multiset.mem_cons, mem_insert] using h
no goals
α : Type u_1
β : α → Type u
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : ¬a ∈ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ cons s a b e₁ e (_ : e ∈ insert a s) = cons s a b e₂ e (_ : e ∈ insert a s)
rw [eq]