no goals
a b : Prop
l : List Prop
h : b ∈ l
H : TFAE (a :: l)
⊢ a ∈ a :: l
simp
case intro.head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
⊢ a ↔ a

case intro.head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
q : Prop
hq : Mem q l
⊢ a ↔ q

case intro.tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
p : Prop
hp : Mem p l
⊢ p ↔ a

case intro.tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ TFAE l → TFAE (a :: l)
rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
no goals
case intro.head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
⊢ a ↔ a
rfl
no goals
case intro.head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
q : Prop
hq : Mem q l
⊢ a ↔ q
exact ab.trans (H _ h _ hq)
no goals
case intro.tail.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
p : Prop
hp : Mem p l
⊢ p ↔ a
exact (ab.trans (H _ h _ hp)).symm
no goals
case intro.tail.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
p : Prop
hp : Mem p l
q : Prop
hq : Mem q l
⊢ p ↔ q
exact H _ hp _ hq