case nil
a✝ b✝ a b : Prop
⊢ (a → b) → (ilast' b [] → a) → (a ↔ b)

case cons
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
⊢ (a → b) ∧ (b → c) ∧ Chain (fun x x_1 => x → x_1) c l → (ilast' b (c :: l) → a) → (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
a b : Prop
l : List Prop
⊢ Chain (fun x x_1 => x → x_1) a (b :: l) → (ilast' b l → a) → TFAE (a :: b :: l)
induction' l with c l IH generalizing a b <;>
  simp only [tfae_cons_cons, tfae_singleton, and_true_iff, chain_cons, Chain.nil] at *
case cons.intro.intro
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
ab : a → b
bc : b → c
ch : Chain (fun x x_1 => x → x_1) c l
la : ilast' b (c :: l) → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
case cons
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
⊢ (a → b) ∧ (b → c) ∧ Chain (fun x x_1 => x → x_1) c l → (ilast' b (c :: l) → a) → (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
rintro ⟨ab, ⟨bc, ch⟩⟩ la
case cons.intro.intro
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
ab : a → b
bc : b → c
ch : Chain (fun x x_1 => x → x_1) c l
la : ilast' b (c :: l) → a
this : (b ↔ c) ∧ TFAE (c :: l)
⊢ (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
case cons.intro.intro
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
ab : a → b
bc : b → c
ch : Chain (fun x x_1 => x → x_1) c l
la : ilast' b (c :: l) → a
⊢ (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
have := IH ⟨bc, ch⟩ (ab ∘ la)
no goals
case cons.intro.intro
a✝ b✝ c : Prop
l : List Prop
a b : Prop
IH : ∀ {a b : Prop}, (a → b) ∧ Chain (fun x x_1 => x → x_1) b l → (ilast' b l → a) → (a ↔ b) ∧ TFAE (b :: l)
ab : a → b
bc : b → c
ch : Chain (fun x x_1 => x → x_1) c l
la : ilast' b (c :: l) → a
this : (b ↔ c) ∧ TFAE (c :: l)
⊢ (a ↔ b) ∧ (b ↔ c) ∧ TFAE (c :: l)
exact ⟨⟨ab, la ∘ (this.2 c (Mem.head _) _ (ilast'_mem _ _)).1 ∘ bc⟩, this⟩
case nil
a✝¹ b✝¹ a✝ b✝ : Prop
a : a✝ → b✝
b : ilast' b✝ [] → a✝
⊢ a✝ ↔ b✝
case nil
a✝ b✝ a b : Prop
⊢ (a → b) → (ilast' b [] → a) → (a ↔ b)
intro a b
no goals
case nil
a✝¹ b✝¹ a✝ b✝ : Prop
a : a✝ → b✝
b : ilast' b✝ [] → a✝
⊢ a✝ ↔ b✝
exact Iff.intro a b