awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
h :
  ∀ (k : Fin n.succ),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
⊢ Eq (α := Fin n.succ → α) (vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)))
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1)))

Tactic:
ext k : 1
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
h :
  vecCons (n := n) a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) 0 =
    Function.comp (α := Fin (n + 1)) (vecCons a x) (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1)) 0
h₁ :
  ∀ (hk₀ : k ≠ 0),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k

Tactic:
rcases eq_or_ne k 0 with rfl | hk₀

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
⊢ vecCons (n := n) a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) 0 =
    Function.comp (α := Fin (n + 1)) (vecCons a x) (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1)) 0

Tactic:
simp [Equiv.swap_apply_of_ne_of_ne (Fin.succ_ne_zero i).symm (Fin.succ_ne_zero j).symm]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne, Fin.succ_ne_zero
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
h :
  ∀ (hk₀ : i.succ ≠ 0),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) i.succ =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) i.succ
h₁ :
  ∀ (hki : k ≠ i.succ),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k

Tactic:
rcases eq_or_ne k i.succ with rfl | hki

Premises used: Fin.succ, eq_or_ne, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : i.succ ≠ 0
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) i.succ =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) i.succ

Tactic:
simp
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
h :
  ∀ (hk₀ : j.succ ≠ 0) (hki : j.succ ≠ i.succ),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) j.succ =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) j.succ
h₁ :
  ∀ (hkj : k ≠ j.succ),
    vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
      (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k

Tactic:
rcases eq_or_ne k j.succ with rfl | hkj

Premises used: Fin.succ, eq_or_ne, rfl
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : j.succ ≠ 0
hki : j.succ ≠ i.succ
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) j.succ =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) j.succ

Tactic:
simp
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ (↑k : ℕ) - 1 < n

Tactic:
lia
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ

Tactic:
grind
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ

Tactic:
have hk : k = Fin.succ ⟨k - 1, by lia⟩ := by grind
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
⊢ (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) ≠ i

Tactic:
grind
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
⊢ (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) ≠ j

Tactic:
grind
-- Module: Mathlib.Data.Fin.VecNotation
Goal:
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    vecCons a x ((Equiv.swap i.succ j.succ : (a : Fin (n + 1)) → Fin (n + 1)) k)
h₁ : vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k = vecCons a x k
h₂ :
  vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n).succ =
    vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₃ : (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₄ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n)) = vecCons a x ⟨(↑k : ℕ) - 1, ⋯⟩.succ
h₅ : x ((Equiv.swap i j : (a : Fin n) → Fin n) (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n)) = x ⟨(↑k : ℕ) - 1, ⋯⟩
h₆ h₇ : x (⟨(↑k : ℕ) - 1, ⋯⟩ : Fin n) = x ⟨(↑k : ℕ) - 1, ⋯⟩
⊢ vecCons a (x ∘ (⇑(Equiv.swap i j) : (a : Fin n) → Fin n)) k =
    (vecCons a x ∘ (⇑(Equiv.swap i.succ j.succ) : (a : Fin (n + 1)) → Fin (n + 1))) k

Tactic:
rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hki hkj, hk, cons_val_succ,
    Function.comp_apply, cons_val_succ, Equiv.swap_apply_of_ne_of_ne (by grind) (by grind)]

Premises used: Matrix.cons_val_succ, Equiv.swap_apply_of_ne_of_ne, Function.comp_apply
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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}
unfold :
  (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr x inst ⋯ empty
⊢ recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α = congr x inst ⋯ empty

Tactic:
unfold recEmptyOption

Premises used: FinEnum.recEmptyOption
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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}
h_1 : ∀ (heq : card α = 0), congr pempty inst ⋯ empty = congr x inst ⋯ empty
h_2 :
  ∀ (n : ℕ) (heq : card α = n.succ),
    (let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
      congr x inst ⋯ empty
⊢ (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr x inst ⋯ empty

Tactic:
split
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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
h_1 : pempty = x
⊢ congr pempty inst ⋯ empty = congr x inst ⋯ empty

Tactic:
congr 1
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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:
Subsingleton.allEq _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
    congr x inst ⋯ empty

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

Premises used: Eq.symm, Eq.trans, Nat.noConfusion
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
    congr x inst ⋯ empty

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

Premises used: Eq.symm, Eq.trans, Nat.noConfusion
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 α
lhs : recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α
| recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
lhs
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 α
unfold :
  (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n)))) :
    P α)
| recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α

Tactic:
unfold recEmptyOption

Premises used: FinEnum.recEmptyOption
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 α
unfold :
  (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n)))) :
    P α)
| recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
lhs; unfold recEmptyOption

Premises used: FinEnum.recEmptyOption
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 α
conv :
  (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))
⊢ recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option) α =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
conv => lhs; unfold recEmptyOption

Premises used: FinEnum.recEmptyOption
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 α
h_1 :
  ∀ (heq : card α = 0),
    congr pempty inst ⋯ empty =
      congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
        (insertNone (ULift.{u, 0} (Fin (card α - 1)))
          (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
        inst ⋯
        (option ULift.instFinEnum
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin (card α - 1)))))
h_2 :
  ∀ (n : ℕ) (heq : card α = n.succ),
    (let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
      congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
        (insertNone (ULift.{u, 0} (Fin (card α - 1)))
          (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
        inst ⋯
        (option ULift.instFinEnum
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin (card α - 1)))))
⊢ (match (motive := ℕ → P α) cardeq : card α with
    | 0 => congr pempty inst cardeq empty
    | n.succ =>
      let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
      have this := ⋯;
      congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
split
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

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

Premises used: FinEnum.card, absurd, Nat.lt_irrefl
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

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

Premises used: FinEnum.card, absurd, Nat.lt_irrefl
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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
h_2 :
  ∀ (heq : card α = (card α).pred.succ),
    (let fN : FinEnum (ULift.{u, 0} (Fin (card α).pred)) := ULift.instFinEnum;
      have this : card.{u + 1} (ULift.{u, 0} (Fin (card α).pred)) = (card α).pred := ⋯;
      congr
        (insertNone (ULift.{u, 0} (Fin (card α).pred))
          (↑(↑(finChoice (card α).pred) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α).pred)) + 1)))
        inst ⋯
        (option fN
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin (card α).pred))))) =
      congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
        (insertNone (ULift.{u, 0} (Fin (card α - 1)))
          (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
        inst ⋯
        (option ULift.instFinEnum
          (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
            (ULift.{u, 0} (Fin (card α - 1)))))
⊢ (let fN : FinEnum (ULift.{u, 0} (Fin n)) := ULift.instFinEnum;
    have this := ⋯;
    congr (insertNone (ULift.{u, 0} (Fin n)) (↑(↑(finChoice n) : ℕ) : Fin (card (ULift.{u, 0} (Fin n)) + 1))) inst ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin n))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

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

Premises used: Nat.succ_pred_eq_of_pos, Nat.succ.inj, rfl, Eq.trans
-- Module: Mathlib.Data.FinEnum.Option
Goal:
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 : FinEnum (ULift.{u, 0} (Fin (card α).pred)) := ULift.instFinEnum;
    have this : card.{u + 1} (ULift.{u, 0} (Fin (card α).pred)) = (card α).pred := ⋯;
    congr
      (insertNone (ULift.{u, 0} (Fin (card α).pred))
        (↑(↑(finChoice (card α).pred) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α).pred)) + 1)))
      inst ⋯
      (option fN
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α).pred))))) =
    congr (α := Option (ULift.{u, 0} (Fin (card α - 1))))
      (insertNone (ULift.{u, 0} (Fin (card α - 1)))
        (↑(↑(finChoice (card α - 1)) : ℕ) : Fin (card (ULift.{u, 0} (Fin (card α - 1))) + 1)))
      inst ⋯
      (option ULift.instFinEnum
        (recEmptyOption finChoice (fun {α β : Type u} ↦ congr) empty (fun {α : Type u} ↦ option)
          (ULift.{u, 0} (Fin (card α - 1)))))

Tactic:
rfl