α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ Fintype.card { x // x ∈ Finite.toFinset h } = Fintype.card ↑s
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ Finset.card (Finite.toFinset h) = Fintype.card ↑s
rw [← Finset.card_attach, Finset.attach_eq_univ, ← Fintype.card]
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ (fun x => x ∈ (Finite.toFinset h).val) = s
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ Fintype.card { x // x ∈ Finite.toFinset h } = Fintype.card ↑s
refine' Fintype.card_congr (Equiv.setCongr _)
case h
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
x : α
⊢ (x ∈ fun x => x ∈ (Finite.toFinset h).val) ↔ x ∈ s
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ (fun x => x ∈ (Finite.toFinset h).val) = s
ext x
case h
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
x : α
⊢ x ∈ Finite.toFinset h ↔ x ∈ s
case h
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
x : α
⊢ (x ∈ fun x => x ∈ (Finite.toFinset h).val) ↔ x ∈ s
show x ∈ h.toFinset ↔ x ∈ s
no goals
case h
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
x : α
⊢ x ∈ Finite.toFinset h ↔ x ∈ s
simp