case intro
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ P α
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
case intro.refine'_1
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ ∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β

case intro.refine'_2
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ P PEmpty

case intro.refine'_3
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
case intro
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ P α
refine' Fintype.induction_empty_option _ _ _ α
no goals
case intro.refine'_1
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ ∀ (α β : Type u) [inst : Fintype β], α ≃ β → P α → P β

case intro.refine'_2
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ P PEmpty

case intro.refine'_3
α✝ : Type ?u.8615
β : Type ?u.8618
γ : Type ?u.8621
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 α
⊢ ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
exacts [fun α β _ => of_equiv, h_empty, @h_option]