no goals
α : Type u_1
β : Type u_2
γ : Type ?u.27313
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (↑e.symm ∘ f) ↔ Surjective (↑e.symm ∘ f)
hinj : Injective f
⊢ Surjective f
simpa [Function.comp] using e.surjective.comp (this.1 (e.symm.injective.comp hinj))
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.27313
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (↑e.symm ∘ f) ↔ Surjective (↑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f
simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))