-- Mathlib/Data/List/TFAE.lean
theorem tfae_of_cycle {a b} {l : List Prop} (h_chain : List.Chain (· → ·) a (b :: l))
    (h_last : getLastD l b → a) : TFAE (a :: b :: l)

Proof state:
a b : Prop
l : List Prop
h_chain : Chain (fun x1 x2 => x1 → x2) a (b :: l)
h_last : l.getLastD b → a
⊢ (a :: b :: l).TFAE

Tactic:
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, tfae_singleton, and_true, chain_cons, Chain.nil] 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⟩

Result:
no goals

Proof state:
case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x1 x2 => x1 → x2) b l → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ Chain (fun x1 x2 => x1 → x2) c l
h_last : l.getLastD c → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩

Result:
case cons.intro.intro
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x1 x2 => x1 → x2) b l → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : Chain (fun x1 x2 => x1 → x2) c l
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Proof state:
case cons.intro.intro
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x1 x2 => x1 → x2) b l → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : Chain (fun x1 x2 => x1 → x2) c l
this : (b ↔ c) ∧ (c :: l).TFAE
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ (getLastD_mem_cons _ _)).1 ∘ bc⟩, this⟩

Result:
no goals

Proof state:
case cons.intro.intro
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x1 x2 => x1 → x2) b l → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : Chain (fun x1 x2 => x1 → x2) c l
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Tactic:
have := IH ⟨bc, ch⟩ (ab ∘ h_last)

Result:
case cons.intro.intro
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x1 x2 => x1 → x2) b l → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_last : l.getLastD c → a
ab : a → b
bc : b → c
ch : Chain (fun x1 x2 => x1 → x2) c l
this : (b ↔ c) ∧ (c :: l).TFAE
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Proof state:
case cons
c : Prop
l : List Prop
IH : ∀ {a b : Prop}, Chain (fun x1 x2 => x1 → x2) a (b :: l) → (l.getLastD b → a) → (a :: b :: l).TFAE
a b : Prop
h_chain : Chain (fun x1 x2 => x1 → x2) a (b :: c :: l)
h_last : (c :: l).getLastD b → a
⊢ (a :: b :: c :: l).TFAE

Tactic:
simp only [tfae_cons_cons, getLastD_cons, tfae_singleton, and_true, chain_cons, Chain.nil] at *

Result:
case cons
c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x1 x2 => x1 → x2) b l → (l.getLastD b → a) → (a ↔ b) ∧ (b :: l).TFAE
h_chain : (a → b) ∧ (b → c) ∧ Chain (fun x1 x2 => x1 → x2) c l
h_last : l.getLastD c → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ (c :: l).TFAE

Proof state:
case nil
a b : Prop
h_chain : Chain (fun x1 x2 => x1 → x2) a [b]
h_last : [].getLastD b → a
⊢ [a, b].TFAE

Tactic:
simp_all [tfae_cons_cons, iff_def]

Result:
no goals