Theorem: equiv_fin_of_partENat_card_eq (Jordan/Mathlib/Extensions.lean)

State before:
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
⊢ Nonempty (Fin m ≃ α)
Tactic:
cases' fintypeOrInfinite α with h h
State after:
case inl
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Fintype α
⊢ Nonempty (Fin m ≃ α)

case inr
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)

State before:
case inl
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Fintype α
⊢ Nonempty (Fin m ≃ α)
Tactic:
simp only [PartENat.card_eq_coe_fintype_card, PartENat.natCast_inj] at hα
State after:
case inl
α : Type u_1
m : ℕ
h : Fintype α
hα : Fintype.card α = m
⊢ Nonempty (Fin m ≃ α)

State before:
case inl
α : Type u_1
m : ℕ
h : Fintype α
hα : Fintype.card α = m
⊢ Nonempty (Fin m ≃ α)
Tactic:
exact ⟨(Fintype.equivFinOfCardEq hα).symm⟩
State after:
no goals

State before:
case inr
α : Type u_1
m : ℕ
hα : PartENat.card α = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)
Tactic:
rw [PartENat.card_eq_top_of_infinite] at hα
State after:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)

State before:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ Nonempty (Fin m ≃ α)
Tactic:
exfalso
State after:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ False

State before:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ False
Tactic:
apply PartENat.natCast_ne_top m
State after:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ ↑m = ⊤

State before:
case inr
α : Type u_1
m : ℕ
hα : ⊤ = ↑m
h : Infinite α
⊢ ↑m = ⊤
Tactic:
rw [hα]
State after:
no goals