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

State before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ Nonempty (Fin m ↪ α)
Tactic:
suffices Nonempty (ULift (Fin m) ↪ α) by
  obtain ⟨x'⟩ := this;
  use Equiv.ulift.symm.toEmbedding.trans x'
  apply Function.Embedding.injective
State after:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ Nonempty (ULift.{?u.347, 0} (Fin m) ↪ α)

State before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ Nonempty (ULift.{?u.347, 0} (Fin m) ↪ α)
Tactic:
rw [← Cardinal.le_def, Cardinal.mk_fintype, Fintype.card_ulift, Fintype.card_fin]
State after:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ ↑m ≤ Cardinal.mk α

State before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
⊢ ↑m ≤ Cardinal.mk α
Tactic:
exact Iff.mp Cardinal.natCast_le_toPartENat_iff hα
State after:
no goals

State before:
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
this : Nonempty (ULift.{?u.347, 0} (Fin m) ↪ α)
⊢ Nonempty (Fin m ↪ α)
Tactic:
obtain ⟨x'⟩ := this
State after:
case intro
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Nonempty (Fin m ↪ α)

State before:
case intro
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Nonempty (Fin m ↪ α)
Tactic:
use Equiv.ulift.symm.toEmbedding.trans x'
State after:
case inj'
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Function.Injective ⇑(Function.Embedding.trans (Equiv.toEmbedding Equiv.ulift.symm) x')

State before:
case inj'
α : Type u_1
m : ℕ
hα : ↑m ≤ PartENat.card α
x' : ULift.{?u.347, 0} (Fin m) ↪ α
⊢ Function.Injective ⇑(Function.Embedding.trans (Equiv.toEmbedding Equiv.ulift.symm) x')
Tactic:
apply Function.Embedding.injective
State after:
no goals