English
If there is a cycle of implications among a, b and l with a suitable chain and a last-link condition, then a :: b :: l has TFAE.
Русский
При наличии цикла импликаций между a, b и l, удовлетворяющего цепи и условию последней связи, список a :: b :: l обладает TFAE.
LaTeX
$$$ (h\_chain : List.IsChain (\to) (a :: b :: l)) \land (h\_last : getLastD l b \to a) \Rightarrow \text{TFAE}(a :: b :: l) $$$
Lean4
theorem tfae_of_cycle {a b} {l : List Prop} (h_chain : List.IsChain (· → ·) (a :: b :: l)) (h_last : getLastD l b → a) :
TFAE (a :: b :: l) := by
induction l generalizing a b with
| nil => simp_all [tfae_cons_cons, iff_def]
| cons c l IH =>
simp only [tfae_cons_cons, getLastD_cons, isChain_cons_cons] at *
rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
have := IH ⟨bc, ch⟩ (ab ∘ h_last)
exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩
