Theorem: front?_isSome (Algorithm/Data/Classes/ToList.lean)

State before:
C✝ : Type u_1
α✝ : Type u_2
C : Type u_3
α : Type u_4
inst✝¹ : ToList C α
inst✝ : Front C α
c : C
h : ¬isEmpty c = true
⊢ (front? c).isSome = true
Tactic:
rwa [front?_def, List.head?_isSome, ← List.not_isEmpty_iff_ne_nil, isEmpty_toList]
State after:
no goals