[GOAL]
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ all [] p = true ↔ ∀ (a : α), a ∈ [] → p a = true
[PROOFSTEP]
exact iff_of_true rfl (forall_mem_nil _)
[GOAL]
case cons
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l✝ : List α
a✝ : α
p : α → Bool
a : α
l : List α
ih : all l p = true ↔ ∀ (a : α), a ∈ l → p a = true
⊢ all (a :: l) p = true ↔ ∀ (a_1 : α), a_1 ∈ a :: l → p a_1 = true
[PROOFSTEP]
simp only [all_cons, Bool.and_coe_iff, ih, forall_mem_cons]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
a : α
⊢ (all l fun a => decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a
[PROOFSTEP]
simp only [all_iff_forall, Bool.of_decide_iff]
[GOAL]
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ any l p = true ↔ ∃ a, a ∈ l ∧ p a = true
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l : List α
a : α
p : α → Bool
⊢ any [] p = true ↔ ∃ a, a ∈ [] ∧ p a = true
[PROOFSTEP]
exact iff_of_false Bool.not_false' (not_exists_mem_nil _)
[GOAL]
case cons
α : Type u_1
p✝ : α → Prop
inst✝ : DecidablePred p✝
l✝ : List α
a✝ : α
p : α → Bool
a : α
l : List α
ih : any l p = true ↔ ∃ a, a ∈ l ∧ p a = true
⊢ any (a :: l) p = true ↔ ∃ a_1, a_1 ∈ a :: l ∧ p a_1 = true
[PROOFSTEP]
simp only [any_cons, Bool.or_coe_iff, ih, exists_mem_cons_iff]
[GOAL]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l : List α
a : α
⊢ (any l fun a => decide (p a)) = true ↔ ∃ a, a ∈ l ∧ p a
[PROOFSTEP]
simp [any_iff_exists]
