[GOAL]
p : Prop
⊢ TFAE [p]
[PROOFSTEP]
simp [TFAE, -eq_iff_iff]
[GOAL]
a b : Prop
l : List Prop
h : b ∈ l
H : TFAE (a :: l)
⊢ a ∈ a :: l
[PROOFSTEP]
simp
[GOAL]
a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ TFAE l → TFAE (a :: l)
[PROOFSTEP]
rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
[GOAL]
case intro.head.head
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : TFAE l
⊢ a ↔ a
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
exact ab.trans (H _ h _ hq)
[GOAL]
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
[PROOFSTEP]
exact (ab.trans (H _ h _ hp)).symm
[GOAL]
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
[PROOFSTEP]
exact H _ hp _ hq
[GOAL]
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)
[PROOFSTEP]
induction' l with c l IH generalizing a b
[GOAL]
case nil
a✝ b✝ a b : Prop
⊢ Chain (fun x x_1 => x → x_1) a [b] → (ilast' b [] → a) → TFAE [a, b]
[PROOFSTEP]
simp only [tfae_cons_cons, tfae_singleton, and_true_iff, chain_cons, Chain.nil] at *
[GOAL]
case cons
a✝ b✝ c : Prop
l : List Prop
IH : ∀ {a b : Prop}, Chain (fun x x_1 => x → x_1) a (b :: l) → (ilast' b l → a) → TFAE (a :: b :: l)
a b : Prop
⊢ Chain (fun x x_1 => x → x_1) a (b :: c :: l) → (ilast' b (c :: l) → a) → TFAE (a :: b :: c :: l)
[PROOFSTEP]
simp only [tfae_cons_cons, tfae_singleton, and_true_iff, chain_cons, Chain.nil] at *
[GOAL]
case nil
a✝ b✝ a b : Prop
⊢ (a → b) → (ilast' b [] → a) → (a ↔ b)
[PROOFSTEP]
intro a b
[GOAL]
case nil
a✝¹ b✝¹ a✝ b✝ : Prop
a : a✝ → b✝
b : ilast' b✝ [] → a✝
⊢ a✝ ↔ b✝
[PROOFSTEP]
exact Iff.intro a b
[GOAL]
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)
[PROOFSTEP]
rintro ⟨ab, ⟨bc, ch⟩⟩ la
[GOAL]
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)
[PROOFSTEP]
have := IH ⟨bc, ch⟩ (ab ∘ la)
[GOAL]
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)
[PROOFSTEP]
exact ⟨⟨ab, la ∘ (this.2 c (Mem.head _) _ (ilast'_mem _ _)).1 ∘ bc⟩, this⟩
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ TFAE (map (fun p => ∀ (a : α), p a) l)
[PROOFSTEP]
simp_rw [TFAE, List.forall_mem_map_iff]
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∀ (a : α), j a) ↔ ∀ (a : α), j_1 a)
[PROOFSTEP]
intros p₁ hp₁ p₂ hp₂
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∀ (a : α), p₁ a) ↔ ∀ (a : α), p₂ a
[PROOFSTEP]
exact forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁) (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ TFAE (map (fun p => ∃ a, p a) l)
[PROOFSTEP]
simp_rw [TFAE, List.forall_mem_map_iff]
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
⊢ ∀ (j : α → Prop), j ∈ l → ∀ (j_1 : α → Prop), j_1 ∈ l → ((∃ a, j a) ↔ ∃ a, j_1 a)
[PROOFSTEP]
intros p₁ hp₁ p₂ hp₂
[GOAL]
α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), TFAE (map (fun p => p a) l)
p₁ : α → Prop
hp₁ : p₁ ∈ l
p₂ : α → Prop
hp₂ : p₂ ∈ l
⊢ (∃ a, p₁ a) ↔ ∃ a, p₂ a
[PROOFSTEP]
exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁) (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)
