α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
⊢ Surjective f
intro x
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
⊢ ∃ a, f a = x
have := Classical.propDecidable
case intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
⊢ ∃ a, f a = x
cases nonempty_fintype α
case intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x
case intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
⊢ ∃ a, f a = x
have h₁ : image f univ = univ :=
  eq_of_subset_of_card_le (subset_univ _)
    ((card_image_of_injective univ hinj).symm ▸ le_rfl)
case intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x
case intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
⊢ ∃ a, f a = x
have h₂ : x ∈ image f univ := h₁.symm ▸ mem_univ x
case intro.intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : y ∈ univ ∧ f y = x
⊢ ∃ a, f a = x
case intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
⊢ ∃ a, f a = x
obtain ⟨y, h⟩ := mem_image.1 h₂
no goals
case intro.intro
α : Type u_1
β : Type ?u.26048
γ : Type ?u.26051
inst✝ : Finite α
f : α → α
hinj : Injective f
x : α
this : (a : Prop) → Decidable a
val✝ : Fintype α
h₁ : image f univ = univ
h₂ : x ∈ image f univ
y : α
h : y ∈ univ ∧ f y = x
⊢ ∃ a, f a = x
exact ⟨y, h.2⟩