-- Mathlib/Data/FinEnum/Option.lean
theorem recEmptyOption_of_card_eq_zero {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 : card α = 0) (_ : FinEnum PEmpty.{u + 1}) :
    recEmptyOption finChoice congr empty option α =
      congr _ _ (h.trans card_eq_zero.symm) empty

Proof state:
case h_1.e_x
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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ pempty = x✝

Tactic:
exact Subsingleton.allEq _ _

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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
⊢ recEmptyOption finChoice (fun {α β} => congr) empty (fun {α} => option) α = congr x✝ inst✝ ⋯ empty

Tactic:
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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
⊢ (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 x✝ inst✝ ⋯ empty

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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
⊢ (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 x✝ inst✝ ⋯ empty

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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty = congr x✝ inst✝ ⋯ empty

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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
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 x✝ inst✝ ⋯ empty

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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ congr pempty inst✝ ⋯ empty = congr x✝ inst✝ ⋯ empty

Tactic:
congr 1

Result:
case h_1.e_x
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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
heq✝ : card α = 0
⊢ pempty = x✝

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 : card α = 0
x✝ : FinEnum PEmpty.{u + 1}
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 x✝ inst✝ ⋯ empty

Tactic:
exact Nat.noConfusion <| h.symm.trans ‹_›

Result:
no goals