Theorem: Array.ext'_iff (LeanColls/Data/Array.lean)

State before:
α : Type u_1
A B : Array α
⊢ A = B ↔ A.data = B.data
Tactic:
cases A
State after:
case mk
α : Type u_1
B : Array α
data✝ : List α
⊢ { data := data✝ } = B ↔ { data := data✝ }.data = B.data

State before:
case mk
α : Type u_1
B : Array α
data✝ : List α
⊢ { data := data✝ } = B ↔ { data := data✝ }.data = B.data
Tactic:
cases B
State after:
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
⊢ { data := data✝¹ } = { data := data✝ } ↔ { data := data✝¹ }.data = { data := data✝ }.data

State before:
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
⊢ { data := data✝¹ } = { data := data✝ } ↔ { data := data✝¹ }.data = { data := data✝ }.data
Tactic:
simp
State after:
no goals