Theorem: LeanColls.Fold.any_iff_exists (LeanColls/Classes/Ops/Fold.lean)

State before:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ any f c = true ↔ ∃ x ∈ c, f x = true
Tactic:
rw [any_eq_any_toList]
State after:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ (toList c).any f = true ↔ ∃ x ∈ c, f x = true

State before:
C : Type u_2
τ : Type u_1
inst✝⁶ : Fold C τ
inst✝⁵ : LeanColls.ToList C τ
inst✝⁴ : ToList C τ
inst✝³ : Membership τ C
inst✝² : LeanColls.ToList C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
f : τ → Bool
c : C
⊢ (toList c).any f = true ↔ ∃ x ∈ c, f x = true
Tactic:
simp [Mem.ToList.mem_iff_mem_toList]
State after:
no goals