case inl
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Finite s
⊢ ncard (insert a (s \ {b})) = ncard s

case inr
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Infinite s
⊢ ncard (insert a (s \ {b})) = ncard s
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
⊢ ncard (insert a (s \ {b})) = ncard s
cases' s.finite_or_infinite with h h
no goals
case inr
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Infinite s
⊢ ncard (insert a (s \ {b})) = ncard s
rw [((h.diff (Set.toFinite {b})).mono (subset_insert _ _)).ncard, h.ncard]
case inl
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Finite s
this : Finite ↑s
⊢ ncard (insert a (s \ {b})) = ncard s
case inl
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Finite s
⊢ ncard (insert a (s \ {b})) = ncard s
haveI := h.to_subtype
case inl
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Finite s
this : Finite ↑s
⊢ ¬a ∈ s \ {b}
case inl
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Finite s
this : Finite ↑s
⊢ ncard (insert a (s \ {b})) = ncard s
rw [ncard_insert_of_not_mem, ncard_diff_singleton_add_one hb]
no goals
case inl
α : Type u_1
β : Type ?u.20177
s t : Set α
a b x y : α
f : α → β
ha : ¬a ∈ s
hb : b ∈ s
h : Set.Finite s
this : Finite ↑s
⊢ ¬a ∈ s \ {b}
simp [mem_diff, not_and, not_not, ha]