no goals
α : Type u_1
β : Sort ?u.22986
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
⊢ card as ≤ card (a :: as)
cases Decidable.em (a ∈ as) with
| inl h => simp [h, Nat.le_refl]
| inr h => simp [h, Nat.le_succ]
no goals
case inl
α : Type u_1
β : Sort ?u.22986
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : a ∈ as
⊢ card as ≤ card (a :: as)
simp [h, Nat.le_refl]
no goals
case inr
α : Type u_1
β : Sort ?u.22986
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
as : List α
h : ¬a ∈ as
⊢ card as ≤ card (a :: as)
simp [h, Nat.le_succ]