Theorem: front_def (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
⊢ some (front c h) = some ((front? c).get ⋯)
Tactic:
simpa using (front_mem c h).symm
State after:
no goals