English
Similarly, the odd-indexed position i+i+1 corresponds to the Alt1-construction.
Русский
Аналогично, нечётная позиция i+i+1 соответствует Alt1-конструкциям.
LaTeX
$$$\\operatorname{cons\\_vecBit1\\_eq\\_alt1}(x,u,i) :$$
Lean4
/-- For a type with positive `card`, the recursion principle evaluates to whatever
`congr` makes of the step result, where `Option.none` has been inserted into the
`(finChoice (card α - 1))`th rank of the enumeration.
-/
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))) :=
by
conv => lhs; unfold recEmptyOption
split
· exact absurd (‹_› ▸ h) (card α).lt_irrefl
· rcases Nat.succ.inj <| (card α).succ_pred_eq_of_pos h |>.trans ‹_› with rfl; rfl
