α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ Finset.card (Finite.toFinset hs) = n
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = n
rw [ncard_eq_toFinset_card _ hs]
case hf
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (a : α), a ∈ Finite.toFinset hs → ∃ i h, ?f i h = a

case hf'
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i : ℕ) (h : i < n), ?f i h ∈ Finite.toFinset hs

case f_inj
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i j : ℕ) (hi : i < n) (hj : j < n), ?f i hi = ?f j hj → i = j

case f
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ (i : ℕ) → i < n → α
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ Finset.card (Finite.toFinset hs) = n
apply Finset.card_eq_of_bijective
no goals
case hf
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (a : α), a ∈ Finite.toFinset hs → ∃ i h, ?f i h = a

case hf'
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i : ℕ) (h : i < n), ?f i h ∈ Finite.toFinset hs

case f_inj
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i j : ℕ) (hi : i < n) (hj : j < n), ?f i hi = ?f j hj → i = j

case f
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ (i : ℕ) → i < n → α
all_goals simpa
no goals
case f_inj
α : Type u_1
β : Type ?u.71917
s t : Set α
a b x y : α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
simpa