/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.fintype.option
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Option

/-!
# fintype instances for option
-/


open Function

open Nat

universe u v

variable {α: Type ?u.8616
α β: Type ?u.3533
β γ: Type ?u.8
γ : Type _: Type (?u.2694+1)
Type _}

open Finset Function

instance: {α : Type u_1} → [inst : Fintype α] → Fintype (Option α)
instance {α: Type ?u.20
α : Type _: Type (?u.20+1)
Type _} [Fintype: Type ?u.23 → Type ?u.23
Fintype α: Type ?u.20
α] : Fintype: Type ?u.26 → Type ?u.26
Fintype (Option: Type ?u.27 → Type ?u.27
Option α: Type ?u.20
α) :=
  ⟨Finset.insertNone: {α : Type ?u.38} → Finset α ↪o Finset (Option α)
Finset.insertNone univ: {α : Type ?u.217} → [inst : Fintype α] → Finset α
univ, fun a: ?m.272
a => by
Goals accomplished! 🐙 α✝: Type ?u.11

β: Type ?u.14

γ: Type ?u.17

α: Type ?u.20

inst✝: Fintype α

a: Option α

a ∈ ↑insertNone univsimp
Goals accomplished! 🐙⟩

theorem univ_option: ∀ (α : Type u_1) [inst : Fintype α], univ = ↑insertNone univ
univ_option (α: Type u_1
α : Type _: Type (?u.2338+1)
Type _) [Fintype: Type ?u.2341 → Type ?u.2341
Fintype α: Type ?u.2338
α] : (univ: {α : Type ?u.2348} → [inst : Fintype α] → Finset α
univ : Finset: Type ?u.2346 → Type ?u.2346
Finset (Option: Type ?u.2347 → Type ?u.2347
Option α: Type ?u.2338
α)) = insertNone: {α : Type ?u.2389} → Finset α ↪o Finset (Option α)
insertNone univ: {α : Type ?u.2568} → [inst : Fintype α] → Finset α
univ :=
  rfl: ∀ {α : Sort ?u.2685} {a : α}, a = a
rfl
#align univ_option univ_option: ∀ (α : Type u_1) [inst : Fintype α], univ = ↑insertNone univ
univ_option

@[simp]
theorem Fintype.card_option: ∀ {α : Type u_1} [inst : Fintype α], card (Option α) = card α + 1
Fintype.card_option {α: Type ?u.2703
α : Type _: Type (?u.2703+1)
Type _} [Fintype: Type ?u.2706 → Type ?u.2706
Fintype α: Type ?u.2703
α] :
    Fintype.card: (α : Type ?u.2710) → [inst : Fintype α] → ℕ
Fintype.card (Option: Type ?u.2711 → Type ?u.2711
Option α: Type ?u.2703
α) = Fintype.card: (α : Type ?u.2728) → [inst : Fintype α] → ℕ
Fintype.card α: Type ?u.2703
α + 1: ?m.2734
1 :=
  (Finset.card_cons: ∀ {α : Type ?u.2798} {s : Finset α} {a : α} (h : ¬a ∈ s), Finset.card (cons a s h) = Finset.card s + 1
Finset.card_cons (by
Goals accomplished! 🐙 α✝: Type ?u.2694

β: Type ?u.2697

γ: Type ?u.2700

α: Type u_1

inst✝: Fintype α

¬none ∈ map Embedding.some univsimp
Goals accomplished! 🐙)).trans: ∀ {α : Sort ?u.2803} {a b c : α}, a = b → b = c → a = c
trans <| congr_arg₂: ∀ {α : Sort ?u.2828} {β : Sort ?u.2829} {γ : Sort ?u.2830} (f : α → β → γ) {x x' : α} {y y' : β},
  x = x' → y = y' → f x y = f x' y'
congr_arg₂ _: ?m.2831 → ?m.2832 → ?m.2833
_ (card_map: ∀ {α : Type ?u.2847} {β : Type ?u.2848} {s : Finset α} (f : α ↪ β), Finset.card (map f s) = Finset.card s
card_map _: ?m.2849 ↪ ?m.2850
_) rfl: ∀ {α : Sort ?u.2859} {a : α}, a = a
rfl
#align fintype.card_option Fintype.card_option: ∀ {α : Type u_1} [inst : Fintype α], Fintype.card (Option α) = Fintype.card α + 1
Fintype.card_option

/-- If `Option α` is a `Fintype` then so is `α` -/
def fintypeOfOption: {α : Type u_1} → [inst : Fintype (Option α)] → Fintype α
fintypeOfOption {α: Type ?u.3539
α : Type _: Type (?u.3539+1)
Type _} [Fintype: Type ?u.3542 → Type ?u.3542
Fintype (Option: Type ?u.3543 → Type ?u.3543
Option α: Type ?u.3539
α)] : Fintype: Type ?u.3546 → Type ?u.3546
Fintype α: Type ?u.3539
α :=
  ⟨Finset.eraseNone: {α : Type ?u.3557} → Finset (Option α) →o Finset α
Finset.eraseNone (Fintype.elems: {α : Type ?u.3596} → [self : Fintype α] → Finset α
Fintype.elems (α := Option: Type ?u.3597 → Type ?u.3597
Option α: Type ?u.3539
α)), fun x: ?m.3604
x =>
    mem_eraseNone: ∀ {α : Type ?u.3609} {s : Finset (Option α)} {x : α}, x ∈ ↑eraseNone s ↔ some x ∈ s
mem_eraseNone.mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr (Fintype.complete: ∀ {α : Type ?u.3629} [self : Fintype α] (x : α), x ∈ Fintype.elems
Fintype.complete (some: {α : Type ?u.3632} → α → Option α
some x: ?m.3604
x))⟩
#align fintype_of_option fintypeOfOption: {α : Type u_1} → [inst : Fintype (Option α)] → Fintype α
fintypeOfOption

/-- A type is a `Fintype` if its successor (using `Option`) is a `Fintype`. -/
def fintypeOfOptionEquiv: {α : Type u_1} → {β : Type u_2} → [inst : Fintype α] → α ≃ Option β → Fintype β
fintypeOfOptionEquiv [Fintype: Type ?u.3680 → Type ?u.3680
Fintype α: Type ?u.3671
α] (f: α ≃ Option β
f : α: Type ?u.3671
α ≃ Option: Type ?u.3685 → Type ?u.3685
Option β: Type ?u.3674
β) : Fintype: Type ?u.3688 → Type ?u.3688
Fintype β: Type ?u.3674
β :=
  haveI := Fintype.ofEquiv: {β : Type ?u.3695} → (α : Type ?u.3694) → [inst : Fintype α] → α ≃ β → Fintype β
Fintype.ofEquiv _: Type ?u.3694
_ f: α ≃ Option β
f
  fintypeOfOption: {α : Type ?u.3734} → [inst : Fintype (Option α)] → Fintype α
fintypeOfOption
#align fintype_of_option_equiv fintypeOfOptionEquiv: {α : Type u_1} → {β : Type u_2} → [inst : Fintype α] → α ≃ Option β → Fintype β
fintypeOfOptionEquiv

namespace Fintype

/-- A recursor principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
def truncRecEmptyOption: {P : Type u → Sort v} →
  ({α β : Type u} → α ≃ β → P α → P β) →
    P PEmpty →
      ({α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)) →
        (α : Type u) → [inst : Fintype α] → [inst : DecidableEq α] → Trunc (P α)
truncRecEmptyOption {P: Type u → Sort v
P : Type u: Type (u+1)
Type u → Sort v: Type v
SortSort v: Type v
 v} (of_equiv: {α β : Type u} → α ≃ β → P α → P β
of_equiv : ∀ {α: ?m.3797
α β: ?m.3800
β}, α: ?m.3797
α ≃ β: ?m.3800
β → P: Type u → Sort v
P α: ?m.3797
α → P: Type u → Sort v
P β: ?m.3800
β)
    (h_empty: P PEmpty
h_empty : P: Type u → Sort v
P PEmpty: Sort ?u.3811
PEmpty) (h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
h_option : ∀ {α: ?m.3815
α} [Fintype: Type ?u.3818 → Type ?u.3818
Fintype α: ?m.3815
α] [DecidableEq: Sort ?u.3821 → Sort (max1?u.3821)
DecidableEq α: ?m.3815
α], P: Type u → Sort v
P α: ?m.3815
α → P: Type u → Sort v
P (Option: Type ?u.3832 → Type ?u.3832
Option α: ?m.3815
α))
    (α: Type u
α : Type u: Type (u+1)
Type u) [Fintype: Type ?u.3837 → Type ?u.3837
Fintype α: Type u
α] [DecidableEq: Sort ?u.3840 → Sort (max1?u.3840)
DecidableEq α: Type u
α] : Trunc: Sort ?u.3849 → Sort ?u.3849
Trunc (P: Type u → Sort v
P α: Type u
α) := by
Goals accomplished! 🐙
  α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P α)suffices ∀ n: ℕ
n : ℕ: Type
ℕ, Trunc: Sort ?u.5499 → Sort ?u.5499
Trunc (P: Type u → Sort v
P (ULift: Type ?u.5500 → Type (max?u.5500?u.5501)
ULift <| Fin: ℕ → Type
Fin n: ℕ
n)) by
    α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P α)apply Trunc.bind: {α : Sort ?u.5508} → {β : Sort ?u.5507} → Trunc α → (α → Trunc β) → Trunc β
Trunc.bind (this: (n : ℕ) → Trunc (P (ULift (Fin n)))
this (Fintype.card: (α : Type ?u.5512) → [inst : Fintype α] → ℕ
Fintype.card α: Type u
α))α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

P (ULift (Fin (card α))) → Trunc (P α)
    α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

Trunc (P α)intro h: P (ULift (Fin (card α)))
hα✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

h: P (ULift (Fin (card α)))

Trunc (P α)
    α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

Trunc (P α)apply Trunc.map: {α : Sort ?u.5528} → {β : Sort ?u.5527} → (α → β) → Trunc α → Trunc β
Trunc.map _: ?m.5529 → ?m.5530
_ (Fintype.truncEquivFin: (α : Type ?u.5532) → [inst : DecidableEq α] → [inst : Fintype α] → Trunc (α ≃ Fin (card α))
Fintype.truncEquivFin α: Type u
α)α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

h: P (ULift (Fin (card α)))

α ≃ Fin (card α) → P α
    α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

Trunc (P α)intro e: ?m.5529
eα✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

h: P (ULift (Fin (card α)))

e: α ≃ Fin (card α)

P α
    α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: (n : ℕ) → Trunc (P (ULift (Fin n)))

Trunc (P α)exact of_equiv: {α β : Type u} → α ≃ β → P α → P β
of_equiv (Equiv.ulift: {α : Type ?u.5566} → ULift α ≃ α
Equiv.ulift.trans: {α : Sort ?u.5571} → {β : Sort ?u.5570} → {γ : Sort ?u.5569} → α ≃ β → β ≃ γ → α ≃ γ
trans e: ?m.5529
e.symm: {α : Sort ?u.5583} → {β : Sort ?u.5582} → α ≃ β → β ≃ α
symm) h: P (ULift (Fin (card α)))
h
Goals accomplished! 🐙
  α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P α)apply ind: (n : ℕ) → Trunc (P (ULift (Fin n)))
ind
Goals accomplished! 🐙 where
    -- porting note: do a manual recursion, instead of `induction` tactic,
    -- to ensure the result is computable
    /-- Internal induction hypothesis -/
    ind: (n : ℕ) → Trunc (P (ULift (Fin n)))
ind : ∀ n: ℕ
n : ℕ: Type
ℕ, Trunc: Sort ?u.3873 → Sort ?u.3873
Trunc (P: Type u → Sort v
P (ULift: Type ?u.3874 → Type (max?u.3874?u.3875)
ULift <| Fin: ℕ → Type
Fin n: ℕ
n))
    | Nat.zero: ℕ
Nat.zero => by
Goals accomplished! 🐙
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P (ULift (Fin zero)))have : card: (α : Type ?u.3970) → [inst : Fintype α] → ℕ
card PEmpty: Sort ?u.3971
PEmpty = card: (α : Type ?u.3985) → [inst : Fintype α] → ℕ
card (ULift: Type ?u.3986 → Type (max?u.3986?u.3987)
ULift (Fin: ℕ → Type
Fin 0: ?m.3989
0)) := α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P (ULift (Fin zero)))by
Goals accomplished! 🐙 α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

card PEmpty = card (ULift (Fin 0))simp only [card_fin: ∀ (n : ℕ), card (Fin n) = n
card_fin, card_pempty: card PEmpty = 0
card_pempty,
                                                                     card_ulift: ∀ (α : Type ?u.4042) [inst : Fintype α], card (ULift α) = card α
card_ulift]
Goals accomplished! 🐙
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P (ULift (Fin zero)))apply Trunc.bind: {α : Sort ?u.4155} → {β : Sort ?u.4154} → Trunc α → (α → Trunc β) → Trunc β
Trunc.bind (truncEquivOfCardEq: {α : Type ?u.4159} →
  {β : Type ?u.4158} →
    [inst : Fintype α] →
      [inst_1 : Fintype β] → [inst_2 : DecidableEq α] → [inst_3 : DecidableEq β] → card α = card β → Trunc (α ≃ β)
truncEquivOfCardEq this: card PEmpty = card (ULift (Fin 0))
this)α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: card PEmpty = card (ULift (Fin 0))

PEmpty ≃ ULift (Fin 0) → Trunc (P (ULift (Fin zero)))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P (ULift (Fin zero)))intro e: PEmpty ≃ ULift (Fin 0)
eα✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: card PEmpty = card (ULift (Fin 0))

e: PEmpty ≃ ULift (Fin 0)

Trunc (P (ULift (Fin zero)))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P (ULift (Fin zero)))apply Trunc.mk: {α : Sort ?u.4538} → α → Trunc α
Trunc.mkα✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

this: card PEmpty = card (ULift (Fin 0))

e: PEmpty ≃ ULift (Fin 0)

aP (ULift (Fin zero))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

Trunc (P (ULift (Fin zero)))refine' of_equiv: {α β : Type u} → α ≃ β → P α → P β
of_equiv e: PEmpty ≃ ULift (Fin 0)
e h_empty: P PEmpty
h_empty
Goals accomplished! 🐙
      | Nat.succ: ℕ → ℕ
Nat.succ n: ℕ
n => by
Goals accomplished! 🐙
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))have : card: (α : Type ?u.4552) → [inst : Fintype α] → ℕ
card (Option: Type ?u.4553 → Type ?u.4553
Option (ULift: Type ?u.4554 → Type (max?u.4554?u.4555)
ULift (Fin: ℕ → Type
Fin n: ℕ
n))) = card: (α : Type ?u.4576) → [inst : Fintype α] → ℕ
card (ULift: Type ?u.4577 → Type (max?u.4577?u.4578)
ULift (Fin: ℕ → Type
Fin n: ℕ
n.succ: ℕ → ℕ
succ)) := α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))by
Goals accomplished! 🐙
            α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))simp only [card_fin: ∀ (n : ℕ), card (Fin n) = n
card_fin, card_option: ∀ {α : Type ?u.4608} [inst : Fintype α], card (Option α) = card α + 1
card_option, card_ulift: ∀ (α : Type ?u.4615) [inst : Fintype α], card (ULift α) = card α
card_ulift]
Goals accomplished! 🐙
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))apply Trunc.bind: {α : Sort ?u.4779} → {β : Sort ?u.4778} → Trunc α → (α → Trunc β) → Trunc β
Trunc.bind (truncEquivOfCardEq: {α : Type ?u.4783} →
  {β : Type ?u.4782} →
    [inst : Fintype α] →
      [inst_1 : Fintype β] → [inst_2 : DecidableEq α] → [inst_3 : DecidableEq β] → card α = card β → Trunc (α ≃ β)
truncEquivOfCardEq this: card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))
this)α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

this: card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))

Option (ULift (Fin n)) ≃ ULift (Fin (succ n)) → Trunc (P (ULift (Fin (succ n))))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))intro e: Option (ULift (Fin n)) ≃ ULift (Fin (succ n))
eα✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

this: card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))

e: Option (ULift (Fin n)) ≃ ULift (Fin (succ n))

Trunc (P (ULift (Fin (succ n))))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))apply Trunc.map: {α : Sort ?u.5283} → {β : Sort ?u.5282} → (α → β) → Trunc α → Trunc β
Trunc.map _: ?m.5284 → ?m.5285
_ (ind: (n : ℕ) → Trunc (P (ULift (Fin n)))
ind n: ℕ
n)α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

this: card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))

e: Option (ULift (Fin n)) ≃ ULift (Fin (succ n))

P (ULift (Fin n)) → P (ULift (Fin (succ n)))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))intro ih: ?m.5284
ihα✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

this: card (Option (ULift (Fin n))) = card (ULift (Fin (succ n)))

e: Option (ULift (Fin n)) ≃ ULift (Fin (succ n))

ih: P (ULift (Fin n))

P (ULift (Fin (succ n)))
          α✝: Type ?u.3783

β: Type ?u.3786

γ: Type ?u.3789

P: Type u → Sort v

of_equiv: {α β : Type u} → α ≃ β → P α → P β

h_empty: P PEmpty

h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)

α: Type u

inst✝¹: Fintype α

inst✝: DecidableEq α

n: ℕ

Trunc (P (ULift (Fin (succ n))))refine' of_equiv: {α β : Type u} → α ≃ β → P α → P β
of_equiv e: Option (ULift (Fin n)) ≃ ULift (Fin (succ n))
e (h_option: {α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)
h_option ih: ?m.5284
ih)
Goals accomplished! 🐙
#align fintype.trunc_rec_empty_option Fintype.truncRecEmptyOption: {P : Type u → Sort v} →
  ({α β : Type u} → α ≃ β → P α → P β) →
    P PEmpty →
      ({α : Type u} → [inst : Fintype α] → [inst : DecidableEq α] → P α → P (Option α)) →
        (α : Type u) → [inst : Fintype α] → [inst : DecidableEq α] → Trunc (P α)
Fintype.truncRecEmptyOption

-- Porting note: due to instance inference issues in `SetTheory.Cardinal.Basic`
-- I had to explicitly name `h_fintype` in order to access it manually.
-- was `[Fintype α]`
/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
@[elab_as_elim]
theorem induction_empty_option: ∀ {P : (α : Type u) → [inst : Fintype α] → Prop},
  (∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β) →
    P PEmpty → (∀ (α : Type u) [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [h_fintype : Fintype α], P α
induction_empty_option {P: (α : Type u) → [inst : Fintype α] → Prop
P : ∀ (α: Type u
α : Type u: Type (u+1)
Type u) [Fintype: Type ?u.7615 → Type ?u.7615
Fintype α: Type u
α], Prop: Type
Prop}
    (of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
of_equiv : ∀ (α: ?m.7621
α β: ?m.7624
β) [Fintype: Type ?u.7627 → Type ?u.7627
Fintype β: ?m.7624
β] (e: α ≃ β
e : α: ?m.7621
α ≃ β: ?m.7624
β), @P: (α : Type u) → [inst : Fintype α] → Prop
P α: ?m.7621
α (@Fintype.ofEquiv: {β : Type ?u.7636} → (α : Type ?u.7635) → [inst : Fintype α] → α ≃ β → Fintype β
Fintype.ofEquiv α: ?m.7621
α β: ?m.7624
β ‹_› e: α ≃ β
e.symm: {α : Sort ?u.7642} → {β : Sort ?u.7641} → α ≃ β → β ≃ α
symm) → @P: (α : Type u) → [inst : Fintype α] → Prop
P β: ?m.7624
β ‹_›)
    (h_empty: P PEmpty
h_empty : P: (α : Type u) → [inst : Fintype α] → Prop
P PEmpty: Sort ?u.7660
PEmpty) (h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
h_option : ∀ (α: ?m.7676
α) [Fintype: Type ?u.7679 → Type ?u.7679
Fintype α: ?m.7676
α], P: (α : Type u) → [inst : Fintype α] → Prop
P α: ?m.7676
α → P: (α : Type u) → [inst : Fintype α] → Prop
P (Option: Type ?u.7688 → Type ?u.7688
Option α: ?m.7676
α)) (α: Type u
α : Type u: Type (u+1)
Type u)
    [h_fintype: Fintype α
h_fintype : Fintype: Type ?u.7704 → Type ?u.7704
Fintype α: Type u
α] : P: (α : Type u) → [inst : Fintype α] → Prop
P α: Type u
α := by
Goals accomplished! 🐙
  α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

P αobtain ⟨p⟩: Trunc (∀ (h : Fintype α), P α)
⟨p: ?m.8016
p⟨p⟩: Trunc (∀ (h : Fintype α), P α)
⟩ :=
    let f_empty: ?m.7723
f_empty := fun i: ?m.7725
i => α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

P αby
Goals accomplished! 🐙 α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

i: Fintype PEmpty

P PEmptyconvert h_empty: P PEmpty
h_empty
Goals accomplished! 🐙
    let h_option: ∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
  (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)
h_option : ∀ {α: Type u
α : Type u: Type (u+1)
Type u} [Fintype: Type ?u.7739 → Type ?u.7739
Fintype α: Type u
α] [DecidableEq: Sort ?u.7742 → Sort (max1?u.7742)
DecidableEq α: Type u
α],
          (∀ (h: Fintype α
h : Fintype: Type ?u.7753 → Type ?u.7753
Fintype α: Type u
α), P: (α : Type u) → [inst : Fintype α] → Prop
P α: Type u
α) → ∀ (h: Fintype (Option α)
h : Fintype: Type ?u.7762 → Type ?u.7762
Fintype (Option: Type ?u.7763 → Type ?u.7763
Option α: Type u
α)), P: (α : Type u) → [inst : Fintype α] → Prop
P (Option: Type ?u.7766 → Type ?u.7766
Option α: Type u
α)  := α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

P αby
Goals accomplished! 🐙
      α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

f_empty:= fun i => ?m.7731 i: ∀ (i : Fintype PEmpty), P PEmpty

∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
  (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)rintro α: Type u
α hα: Fintype α
hα -: DecidableEq α
- Pα: ∀ (h : Fintype α), P α
Pα hα': Fintype (Option α)
hα'α✝¹: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α✝: Type u

h_fintype: Fintype α✝

f_empty:= fun i => ?m.7731 i: ∀ (i : Fintype PEmpty), P PEmpty

α: Type u

hα: Fintype α

Pα: ∀ (h : Fintype α), P α

hα': Fintype (Option α)

P (Option α)
      α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

f_empty:= fun i => ?m.7731 i: ∀ (i : Fintype PEmpty), P PEmpty

∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
  (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)convert h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
h_option α: Type u
α (Pα: ∀ (h : Fintype α), P α
Pα _: Fintype α
_)
Goals accomplished! 🐙
    @truncRecEmptyOption: ∀ {P : Type ?u.7775 → Sort ?u.7774},
  (∀ {α β : Type ?u.7775}, α ≃ β → P α → P β) →
    P PEmpty →
      (∀ {α : Type ?u.7775} [inst : Fintype α] [inst : DecidableEq α], P α → P (Option α)) →
        ∀ (α : Type ?u.7775) [inst : Fintype α] [inst : DecidableEq α], Trunc (P α)
truncRecEmptyOption (fun α: ?m.7777
α => ∀ h: ?m.7780
h, @P: (α : Type u) → [inst : Fintype α] → Prop
P α: ?m.7777
α h: ?m.7780
h) (@fun α: ?m.7788
α β: ?m.7791
β e: ?m.7794
e hα: ?m.7797
hα hβ: ?m.7801
hβ => @of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
of_equiv α: ?m.7788
α β: ?m.7791
β hβ: ?m.7801
hβ e: ?m.7794
e (hα: ?m.7797
hα _: Fintype α
_))
      f_empty: ?m.7723
f_empty h_option: ∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
  (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)
h_option α: Type u
α _ (Classical.decEq: (α : Sort ?u.7992) → DecidableEq α
Classical.decEq α: Type u
α)α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

x✝: Trunc (∀ (h : Fintype α), P α)

p: ∀ (h : Fintype α), P α

mkP α
  α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

P α·α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

x✝: Trunc (∀ (h : Fintype α), P α)

p: ∀ (h : Fintype α), P α

mkP α α✝: Type ?u.7603

β: Type ?u.7606

γ: Type ?u.7609

P: (α : Type u) → [inst : Fintype α] → Prop

of_equiv: ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β

h_empty: P PEmpty

h_option: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)

α: Type u

h_fintype: Fintype α

x✝: Trunc (∀ (h : Fintype α), P α)

p: ∀ (h : Fintype α), P α

mkP αexact p: ?m.8016
p _: Fintype α
_
Goals accomplished! 🐙
  -- ·
#align fintype.induction_empty_option Fintype.induction_empty_option: ∀ {P : (α : Type u) → [inst : Fintype α] → Prop},
  (∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β) →
    P PEmpty → (∀ (α : Type u) [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [h_fintype : Fintype α], P α
Fintype.induction_empty_option

end Fintype

/-- An induction principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
theorem Finite.induction_empty_option: ∀ {P : Type u → Prop},
  (∀ {α β : Type u}, α ≃ β → P α → P β) →
    P PEmpty → (∀ {α : Type u} [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [inst : Finite α], P α
Finite.induction_empty_option {P: Type u → Prop
P : Type u: Type (u+1)
Type u → Prop: Type
Prop} (of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β
of_equiv : ∀ {α: ?m.8630
α β: ?m.8633
β}, α: ?m.8630
α ≃ β: ?m.8633
β → P: Type u → Prop
P α: ?m.8630
α → P: Type u → Prop
P β: ?m.8633
β)
    (h_empty: P PEmpty
h_empty : P: Type u → Prop
P PEmpty: Sort ?u.8644
PEmpty) (h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
h_option : ∀ {α: ?m.8648
α} [Fintype: Type ?u.8651 → Type ?u.8651
Fintype α: ?m.8648
α], P: Type u → Prop
P α: ?m.8648
α → P: Type u → Prop
P (Option: Type ?u.8656 → Type ?u.8656
Option α: ?m.8648
α)) (α: Type u
α : Type u: Type (u+1)
Type u)
    [Finite: Sort ?u.8661 → Prop
Finite α: Type u
α] : P: Type u → Prop
P α: Type u
α := by
Goals accomplished! 🐙
  α✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

P αcases nonempty_fintype: ∀ (α : Type ?u.8673) [inst : Finite α], Nonempty (Fintype α)
nonempty_fintype α: Type u
αα✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

val✝: Fintype α

introP α
  α✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

P αrefine' Fintype.induction_empty_option: ∀ {P : (α : Type ?u.8723) → [inst : Fintype α] → Prop},
  (∀ (α β : Type ?u.8723) [inst : Fintype β] (e : α ≃ β), P α → P β) →
    P PEmpty →
      (∀ (α : Type ?u.8723) [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type ?u.8723) [h_fintype : Fintype α], P α
Fintype.induction_empty_option _: ∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β
_ _: P PEmpty
_ _: ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
_ α: Type u
αα✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

val✝: Fintype α

intro.refine'_1∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β
α✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

val✝: Fintype α

intro.refine'_2P PEmpty
α✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

val✝: Fintype α

intro.refine'_3∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
  α✝: Type ?u.8616

β: Type ?u.8619

γ: Type ?u.8622

P: Type u → Prop

of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β

h_empty: P PEmpty

h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)

α: Type u

inst✝: Finite α

P αexacts[fun α: ?m.8769
α β: ?m.8772
β _: ?m.8775
_ => of_equiv: ∀ {α β : Type u}, α ≃ β → P α → P β
of_equiv, h_empty: P PEmpty
h_empty, @h_option: ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)
h_option]
Goals accomplished! 🐙
#align finite.induction_empty_option Finite.induction_empty_option: ∀ {P : Type u → Prop},
  (∀ {α β : Type u}, α ≃ β → P α → P β) →
    P PEmpty → (∀ {α : Type u} [inst : Fintype α], P α → P (Option α)) → ∀ (α : Type u) [inst : Finite α], P α
Finite.induction_empty_option