/-
Copyright (c) 2022 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen

! This file was ported from Lean 3 source module data.fun_like.fintype
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finite.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.FunLike.Basic

/-!
# Finiteness of `FunLike` types

We show a type `F` with a `FunLike F α β` is finite if both `α` and `β` are finite.
This corresponds to the following two pairs of declarations:

 * `FunLike.fintype` is a definition stating all `FunLike`s are finite if their domain and
   codomain are.
 * `FunLike.finite` is a lemma stating all `FunLike`s are finite if their domain and
   codomain are.
 * `FunLike.fintype'` is a non-dependent version of `FunLike.fintype` and
 * `FunLike.finite` is a non-dependent version of `FunLike.finite`, because dependent instances
   are harder to infer.

You can use these to produce instances for specific `FunLike` types.
(Although there might be options for `Fintype` instances with better definitional behaviour.)
They can't be instances themselves since they can cause loops.
-/

-- porting notes: `Type` is a reserved word, switched to `Type'`
section Type'

variable (F: Type ?u.37
F G: Type ?u.40
G : Type _: Type (?u.37+1)
Type _) {α: Type ?u.43
α γ: Type ?u.46
γ : Type _: Type (?u.43+1)
Type _} {β: α → Type ?u.51
β : α: Type ?u.8
α → Type _: Type (?u.392+1)
Type _} [FunLike: Sort ?u.56 → (α : outParam (Sort ?u.55)) → outParam (α → Sort ?u.54) → Sort (max(max(max1?u.56)?u.55)?u.54)
FunLike F: Type ?u.37
F α: Type ?u.43
α β: α → Type ?u.392
β] [FunLike: Sort ?u.29 → (α : outParam (Sort ?u.28)) → outParam (α → Sort ?u.27) → Sort (max(max(max1?u.29)?u.28)?u.27)
FunLike G: Type ?u.5
G α: Type ?u.8
α fun _: ?m.31
_ => γ: Type ?u.387
γ]

/-- All `FunLike`s are finite if their domain and codomain are.

This is not an instance because specific `FunLike` types might have a better-suited definition.

See also `FunLike.finite`.
-/
noncomputable def FunLike.fintype: (F : Type u_1) →
  {α : Type u_2} →
    {β : α → Type u_3} →
      [inst : FunLike F α β] →
        [inst : DecidableEq α] → [inst : Fintype α] → [inst : (i : α) → Fintype (β i)] → Fintype F
FunLike.fintype [DecidableEq: Sort ?u.72 → Sort (max1?u.72)
DecidableEq α: Type ?u.43
α] [Fintype: Type ?u.81 → Type ?u.81
Fintype α: Type ?u.43
α] [∀ i: ?m.85
i, Fintype: Type ?u.88 → Type ?u.88
Fintype (β: α → Type ?u.51
β i: ?m.85
i)] : Fintype: Type ?u.92 → Type ?u.92
Fintype F: Type ?u.37
F :=
  Fintype.ofInjective: {α : Type ?u.100} → {β : Type ?u.99} → [inst : Fintype β] → (f : α → β) → Function.Injective f → Fintype α
Fintype.ofInjective _: ?m.101 → ?m.102
_ FunLike.coe_injective: ∀ {F : Sort ?u.149} {α : Sort ?u.150} {β : α → Sort ?u.151} [i : FunLike F α β], Function.Injective fun f => ↑f
FunLike.coe_injective
#align fun_like.fintype FunLike.fintype: (F : Type u_1) →
  {α : Type u_2} →
    {β : α → Type u_3} →
      [inst : FunLike F α β] →
        [inst : DecidableEq α] → [inst : Fintype α] → [inst : (i : α) → Fintype (β i)] → Fintype F
FunLike.fintype

/-- All `FunLike`s are finite if their domain and codomain are.

Non-dependent version of `FunLike.fintype` that might be easier to infer.
This is not an instance because specific `FunLike` types might have a better-suited definition.
-/
noncomputable def FunLike.fintype': [inst : DecidableEq α] → [inst : Fintype α] → [inst : Fintype γ] → Fintype G
FunLike.fintype' [DecidableEq: Sort ?u.413 → Sort (max1?u.413)
DecidableEq α: Type ?u.384
α] [Fintype: Type ?u.422 → Type ?u.422
Fintype α: Type ?u.384
α] [Fintype: Type ?u.425 → Type ?u.425
Fintype γ: Type ?u.387
γ] : Fintype: Type ?u.428 → Type ?u.428
Fintype G: Type ?u.381
G :=
  FunLike.fintype: (F : Type ?u.437) →
  {α : Type ?u.436} →
    {β : α → Type ?u.435} →
      [inst : FunLike F α β] →
        [inst : DecidableEq α] → [inst : Fintype α] → [inst : (i : α) → Fintype (β i)] → Fintype F
FunLike.fintype G: Type ?u.381
G
#align fun_like.fintype' FunLike.fintype': (G : Type u_1) →
  {α : Type u_2} →
    {γ : Type u_3} →
      [inst : FunLike G α fun x => γ] → [inst : DecidableEq α] → [inst : Fintype α] → [inst : Fintype γ] → Fintype G
FunLike.fintype'

end Type'

-- porting notes: `Sort` is a reserved word, switched to `Sort'`
section Sort'

variable (F: Sort ?u.578
F G: Sort ?u.616
G : Sort _: Type ?u.578
SortSort _: Type ?u.578
 _) {α: Sort ?u.885
α γ: Sort ?u.622
γ : Sort _: Type ?u.584
SortSort _: Type ?u.584
 _} {β: α → Sort ?u.627
β : α: Sort ?u.885
α → Sort _: Type ?u.893
SortSort _: Type ?u.893
 _} [FunLike: Sort ?u.898 → (α : outParam (Sort ?u.897)) → outParam (α → Sort ?u.896) → Sort (max(max(max1?u.898)?u.897)?u.896)
FunLike F: Sort ?u.879
F α: Sort ?u.619
α β: α → Sort ?u.627
β] [FunLike: Sort ?u.605 → (α : outParam (Sort ?u.604)) → outParam (α → Sort ?u.603) → Sort (max(max(max1?u.605)?u.604)?u.603)
FunLike G: Sort ?u.882
G α: Sort ?u.619
α fun _: ?m.607
_ => γ: Sort ?u.587
γ]

/-- All `FunLike`s are finite if their domain and codomain are.

Can't be an instance because it can cause infinite loops.
-/
theorem FunLike.finite: ∀ (F : Sort u_3) {α : Sort u_1} {β : α → Sort u_2} [inst : FunLike F α β] [inst : Finite α]
  [inst : ∀ (i : α), Finite (β i)], Finite F
FunLike.finite [Finite: Sort ?u.648 → Prop
Finite α: Sort ?u.619
α] [∀ i: ?m.652
i, Finite: Sort ?u.655 → Prop
Finite (β: α → Sort ?u.627
β i: ?m.652
i)] : Finite: Sort ?u.659 → Prop
Finite F: Sort ?u.613
F :=
  Finite.of_injective: ∀ {α : Sort ?u.663} {β : Sort ?u.664} [inst : Finite β] (f : α → β), Function.Injective f → Finite α
Finite.of_injective _: ?m.665 → ?m.666
_ FunLike.coe_injective: ∀ {F : Sort ?u.707} {α : Sort ?u.708} {β : α → Sort ?u.709} [i : FunLike F α β], Function.Injective fun f => ↑f
FunLike.coe_injective
#align fun_like.finite FunLike.finite: ∀ (F : Sort u_3) {α : Sort u_1} {β : α → Sort u_2} [inst : FunLike F α β] [inst : Finite α]
  [inst : ∀ (i : α), Finite (β i)], Finite F
FunLike.finite

/-- All `FunLike`s are finite if their domain and codomain are.

Non-dependent version of `FunLike.finite` that might be easier to infer.
Can't be an instance because it can cause infinite loops.
-/
theorem FunLike.finite': ∀ [inst : Finite α] [inst : Finite γ], Finite G
FunLike.finite' [Finite: Sort ?u.914 → Prop
Finite α: Sort ?u.885
α] [Finite: Sort ?u.917 → Prop
Finite γ: Sort ?u.888
γ] : Finite: Sort ?u.920 → Prop
Finite G: Sort ?u.882
G :=
  FunLike.finite: ∀ (F : Sort ?u.926) {α : Sort ?u.924} {β : α → Sort ?u.925} [inst : FunLike F α β] [inst : Finite α]
  [inst : ∀ (i : α), Finite (β i)], Finite F
FunLike.finite G: Sort ?u.882
G
#align fun_like.finite' FunLike.finite': ∀ (G : Sort u_3) {α : Sort u_1} {γ : Sort u_2} [inst : FunLike G α fun x => γ] [inst : Finite α] [inst : Finite γ],
  Finite G
FunLike.finite'

end Sort'