case pos
α : Type u_1
β : Type ?u.11523
s t : Set α
a b x y : α
f : α → β
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
h : a ∈ s
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1

case neg
α : Type u_1
β : Type ?u.11523
s t : Set α
a b x y : α
f : α → β
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
h : ¬a ∈ s
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
α : Type u_1
β : Type ?u.11523
s t : Set α
a b x y : α
f : α → β
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
by_cases h : a ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.11523
s t : Set α
a b x y : α
f : α → β
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
h : a ∈ s
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
rw [ncard_insert_of_mem h, if_pos h]
no goals
case neg
α : Type u_1
β : Type ?u.11523
s t : Set α
a b x y : α
f : α → β
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
h : ¬a ∈ s
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
rw [ncard_insert_of_not_mem h hs, if_neg h]