case intro
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective f
val✝ : Fintype (PLift β)
⊢ Finite α
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective f
⊢ Finite α
cases nonempty_fintype (PLift β)
case intro
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective (↑Equiv.plift.symm ∘ f ∘ ↑Equiv.plift)
val✝ : Fintype (PLift β)
⊢ Finite α
case intro
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective f
val✝ : Fintype (PLift β)
⊢ Finite α
rw [← Equiv.injective_comp Equiv.plift f, ← Equiv.comp_injective _ Equiv.plift.symm] at H
case intro
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective (↑Equiv.plift.symm ∘ f ∘ ↑Equiv.plift)
val✝ : Fintype (PLift β)
this : Fintype (PLift α)
⊢ Finite α
case intro
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective (↑Equiv.plift.symm ∘ f ∘ ↑Equiv.plift)
val✝ : Fintype (PLift β)
⊢ Finite α
haveI := Fintype.ofInjective _ H
no goals
case intro
α✝ : Type ?u.13191
β✝ : Type ?u.13194
γ : Type ?u.13197
α : Sort u_1
β : Sort u_2
inst✝ : Finite β
f : α → β
H : Injective (↑Equiv.plift.symm ∘ f ∘ ↑Equiv.plift)
val✝ : Fintype (PLift β)
this : Fintype (PLift α)
⊢ Finite α
exact Finite.of_equiv _ Equiv.plift