Theorem: Finite.exists_PartialEquiv_of_encard_eq (Matroid/ForMathlib/PartialEquiv.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
⊢ ∃ e, e.source = s ∧ e.target = t
Tactic:
obtain ⟨f, hf⟩ := hfin.exists_bijOn_of_encard_eq h
State after:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
f : α → β
hf : BijOn f s t
⊢ ∃ e, e.source = s ∧ e.target = t

State before:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Nonempty α
inst✝ : Nonempty β
s : Set α
t : Set β
hfin : s.Finite
h : s.encard = t.encard
f : α → β
hf : BijOn f s t
⊢ ∃ e, e.source = s ∧ e.target = t
Tactic:
exact ⟨hf.toPartialEquiv, rfl, hf.toPartialEquiv_target⟩
State after:
no goals