case pos
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card s - 1 ≤ card (erase s a)

case neg
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card (erase s a)
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card s - 1 ≤ card (erase s a)
by_cases h : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card s - 1 ≤ card (erase s a)
exact (card_erase_of_mem h).ge
case neg
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card s
case neg
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card (erase s a)
rw [erase_eq_of_not_mem h]
no goals
case neg
α : Type u_1
β : Type ?u.7358
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card s
exact Nat.sub_le _ _