Theorem: Fin.nonempty_equiv_iff_encard_eq (Matroid/ForMathlib/Card.lean)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
⊢ Nonempty (↑s ≃ Fin n) ↔ s.encard = ↑n
Tactic:
refine ⟨fun ⟨e⟩ ↦ by simpa using e.encard_univ_eq, fun h ↦ ?_⟩
State after:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
⊢ Nonempty (↑s ≃ Fin n)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
⊢ Nonempty (↑s ≃ Fin n)
Tactic:
have _ := Finite.fintype (finite_of_encard_eq_coe h).to_subtype
State after:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Nonempty (↑s ≃ Fin n)

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Nonempty (↑s ≃ Fin n)
Tactic:
exact ⟨Fintype.equivFinOfCardEq <| by simpa [encard_eq_coe_toFinset_card, Nat.cast_inj] using h⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
x✝ : Nonempty (↑s ≃ Fin n)
e : ↑s ≃ Fin n
⊢ s.encard = ↑n
Tactic:
simpa using e.encard_univ_eq
State after:
no goals

State before:
α : Type u_1
β : Type u_2
s t : Set α
n : ℕ
h : s.encard = ↑n
x✝ : Fintype ↑s
⊢ Fintype.card ↑s = n
Tactic:
simpa [encard_eq_coe_toFinset_card, Nat.cast_inj] using h
State after:
no goals