case inl
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
⊢ ncard s - 1 ≤ ncard (s \ {a})

case inr
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard s - 1 ≤ ncard (s \ {a})
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
⊢ ncard s - 1 ≤ ncard (s \ {a})
cases' s.finite_or_infinite with hs hs
case h.e'_3
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard s - 1 = 0
case inr
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard s - 1 ≤ ncard (s \ {a})
convert Nat.zero_le _
no goals
case h.e'_3
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Infinite s
⊢ ncard s - 1 = 0
rw [hs.ncard]
case pos
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
h : a ∈ s
⊢ ncard s - 1 ≤ ncard (s \ {a})

case neg
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard s - 1 ≤ ncard (s \ {a})
case inl
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
⊢ ncard s - 1 ≤ ncard (s \ {a})
by_cases h : a ∈ s
case neg
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard s - 1 ≤ ncard s
case neg
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard s - 1 ≤ ncard (s \ {a})
rw [diff_singleton_eq_self h]
no goals
case neg
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard s - 1 ≤ ncard s
apply Nat.pred_le
no goals
case pos
α : Type u_1
β : Type ?u.18254
s✝ t : Set α
a✝ b x y : α
f : α → β
s : Set α
a : α
hs : Set.Finite s
h : a ∈ s
⊢ ncard s - 1 ≤ ncard (s \ {a})
rw [ncard_diff_singleton_of_mem h hs]