-- Mathlib/Data/FinEnum/Option.lean
theorem recEmptyOption_of_card_pos {P : Type u → Sort v}
    (finChoice : (n : ℕ) → Fin (n + 1))
    (congr : {α β : Type u} → (_ : FinEnum α) → (_ : FinEnum β) → card β = card α → P α → P β)
    (empty : P PEmpty.{u + 1})
    (option : {α : Type u} → FinEnum α → P α → P (Option α))
    (α : Type u) [FinEnum α] (h : 0 < card α) :
    recEmptyOption finChoice congr empty option α =
      congr (insertNone _ <| finChoice (card α - 1)) ‹_›
        (congrArg (· + 1) card_fin |>.trans <| (card α).succ_pred_eq_of_pos h).symm
        (option ULift.instFinEnum <|
          recEmptyOption finChoice congr empty option (ULift.{u} <| Fin (card α - 1)))

Proof state:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
⊢ (match cardeq : card α with
    | 0 => congr pempty inst✝ cardeq empty
    | n.succ =>
      let fN := ULift.instFinEnum;
      let_fun this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) ↑↑(finChoice n)) inst✝ ⋯
        (option fN (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin n))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
split

Result:
case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    let_fun this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin n✝))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Proof state:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
n✝ : ℕ
heq✝ : card α = n✝.succ
⊢ (let fN := ULift.instFinEnum;
    let_fun this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n✝)) ↑↑(finChoice n✝)) inst✝ ⋯
      (option fN (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin n✝))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
rcases Nat.succ.inj <| (card α).succ_pred_eq_of_pos h |>.trans ‹_› with rfl

Result:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = (card α).pred.succ
⊢ (let fN := ULift.instFinEnum;
    let_fun this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin (card α).pred)) ↑↑(finChoice (card α).pred)) inst✝ ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Proof state:
case h_1
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
exact absurd (‹_› ▸ h) (card α).lt_irrefl

Result:
no goals

Proof state:
case h_2
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
heq✝ : card α = (card α).pred.succ
⊢ (let fN := ULift.instFinEnum;
    let_fun this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin (card α).pred)) ↑↑(finChoice (card α).pred)) inst✝ ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
rfl

Result:
no goals

Proof state:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
⊢ recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) α =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
conv => lhs; unfold recEmptyOption

Result:
P : Type u → Sort v
finChoice : (n : ℕ) → Fin (n + 1)
congr : {α β : Type u} → (x : FinEnum α) → (x_1 : FinEnum β) → card β = card α → P α → P β
empty : P PEmpty.{u + 1}
option : {α : Type u} → FinEnum α → P α → P (Option α)
α : Type u
inst✝ : FinEnum α
h : 0 < card α
⊢ (match cardeq : card α with
    | 0 => congr pempty inst✝ cardeq empty
    | n.succ =>
      let fN := ULift.instFinEnum;
      let_fun this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) ↑↑(finChoice n)) inst✝ ⋯
        (option fN (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin n))))) =
    congr (insertNone (ULift.{u, 0} (Fin (card α - 1))) ↑↑(finChoice (card α - 1))) inst✝ ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) (ULift.{u, 0} (Fin (card α - 1)))))