Theorem: LeanColls.Fold.all_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
⊢ all f c = true ↔ ∀ x ∈ c, f x = true
Tactic:
rw [all_eq_all_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).all 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).all f = true ↔ ∀ x ∈ c, f x = true
Tactic:
simp [Mem.ToList.mem_iff_mem_toList]
State after:
no goals