Theorem: Array.isEmpty_iff_data_eq_nil (Runtime/Utilities/Extensions.lean)

State before:
α : Type u_1
as : Array α
⊢ isEmpty as = true ↔ as.data = []
Tactic:
simp [isEmpty, size]
State after:
α : Type u_1
as : Array α
⊢ List.length as.data = 0 ↔ as.data = []

State before:
α : Type u_1
as : Array α
⊢ List.length as.data = 0 ↔ as.data = []
Tactic:
exact List.length_eq_zero
State after:
no goals