Theorem: List.isEmpty_reverse (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
l : List α
⊢ l.reverse.isEmpty = l.isEmpty
Tactic:
rw [isEmpty_eq_decide_eq_nil, isEmpty_eq_decide_eq_nil]
State after:
C : Type u_1
α : Type u_2
l : List α
⊢ decide (l.reverse = []) = decide (l = [])

State before:
C : Type u_1
α : Type u_2
l : List α
⊢ decide (l.reverse = []) = decide (l = [])
Tactic:
simp only [reverse_eq_nil_iff]
State after:
no goals