case mk
α✝ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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 α
⊢ P α
α✝ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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⟩ :=
  let f_empty := fun i => by convert h_empty
  let h_option : ∀ {α : Type u} [Fintype α] [DecidableEq α],
        (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)  := by
    rintro α hα - Pα hα'
    convert h_option α (Pα _)
  @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
    f_empty h_option α _ (Classical.decEq α)
no goals
α✝ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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 PEmpty
convert h_empty
α✝¹ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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 : ∀ (i : Fintype PEmpty), P PEmpty := fun i => ?m.7730 i
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)
α✝ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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 : ∀ (i : Fintype PEmpty), P PEmpty := fun i => ?m.7730 i
⊢ ∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
    (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)
rintro α hα - Pα hα'
no goals
α✝¹ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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 : ∀ (i : Fintype PEmpty), P PEmpty := fun i => ?m.7730 i
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)
convert h_option α (Pα _)
no goals
case mk
α✝ : Type ?u.7602
β : Type ?u.7605
γ : Type ?u.7608
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 α
⊢ P α
exact p _