-- Mathlib/Data/Fintype/Option.lean
theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
    (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›)
    (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
    [h_fintype : Fintype α] : P α

Proof state:
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := fun i => ?m.4405
⊢ ∀ {α : Type u} [inst : Fintype α] [inst : DecidableEq α],
    (∀ (h : Fintype α), P α) → ∀ (h : Fintype (Option α)), P (Option α)

Tactic:
rintro α hα - Pα hα'

Result:
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α✝ : Type u
h_fintype : Fintype α✝
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := fun i => ?m.4405
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)

Proof state:
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α✝ : Type u
h_fintype : Fintype α✝
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := fun i => ?m.4405
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)

Tactic:
convert h_option α (Pα _)

Result:
no goals

Proof state:
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
⊢ P α

Tactic:
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 α)

Result:
case mk
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
x✝ : Trunc (∀ (h : Fintype α), P α)
p : ∀ (h : Fintype α), P α
⊢ P α

Proof state:
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
i : Fintype PEmpty.{u + 1}
⊢ P PEmpty.{u + 1}

Tactic:
convert h_empty

Result:
no goals

Proof state:
case mk
P : (α : Type u) → [inst : Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α : Type u
h_fintype : Fintype α
x✝ : Trunc (∀ (h : Fintype α), P α)
p : ∀ (h : Fintype α), P α
⊢ P α

Tactic:
exact p _

Result:
no goals