α : Type u_1
β : Type ?u.15901
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) < ncard (s \ {a}) + 1
α : Type u_1
β : Type ?u.15901
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) < ncard s
rw [← ncard_diff_singleton_add_one h hs]
no goals
α : Type u_1
β : Type ?u.15901
s t : Set α
a b x y : α
f : α → β
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) < ncard (s \ {a}) + 1
apply lt_add_one