no goals
α : Type u_1
β : Type ?u.9534
s t : Set α
a b x y : α
f : α → β
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (insert a s) = ncard s + 1
classical
have hft := hs.fintype
rw [ncard_eq_toFinset_card _, ncard_eq_toFinset_card _, Finite.toFinset_insert,
  Finset.card_insert_of_not_mem]
rwa [Finite.mem_toFinset]
α : Type u_1
β : Type ?u.9534
s t : Set α
a b x y : α
f : α → β
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
hft : Fintype ↑s
⊢ ncard (insert a s) = ncard s + 1
α : Type u_1
β : Type ?u.9534
s t : Set α
a b x y : α
f : α → β
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (insert a s) = ncard s + 1
have hft := hs.fintype
α : Type u_1
β : Type ?u.9534
s t : Set α
a b x y : α
f : α → β
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
hft : Fintype ↑s
⊢ ¬a ∈ Finite.toFinset (_ : Set.Finite s)
α : Type u_1
β : Type ?u.9534
s t : Set α
a b x y : α
f : α → β
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
hft : Fintype ↑s
⊢ ncard (insert a s) = ncard s + 1
rw [ncard_eq_toFinset_card _, ncard_eq_toFinset_card _, Finite.toFinset_insert,
  Finset.card_insert_of_not_mem]
no goals
α : Type u_1
β : Type ?u.9534
s t : Set α
a b x y : α
f : α → β
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
hft : Fintype ↑s
⊢ ¬a ∈ Finite.toFinset (_ : Set.Finite s)
rwa [Finite.mem_toFinset]