case mk
α : Type u_1
bs : Array α
data✝ : List α
h : { data := data✝ }.data = bs.data
⊢ { data := data✝ } = bs
α : Type u_1
as bs : Array α
h : as.data = bs.data
⊢ as = bs
cases as
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
h : { data := data✝¹ }.data = { data := data✝ }.data
⊢ { data := data✝¹ } = { data := data✝ }
case mk
α : Type u_1
bs : Array α
data✝ : List α
h : { data := data✝ }.data = bs.data
⊢ { data := data✝ } = bs
cases bs
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
h : data✝¹ = data✝
⊢ { data := data✝¹ } = { data := data✝ }
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
h : { data := data✝¹ }.data = { data := data✝ }.data
⊢ { data := data✝¹ } = { data := data✝ }
simp at h
no goals
case mk.mk
α : Type u_1
data✝¹ data✝ : List α
h : data✝¹ = data✝
⊢ { data := data✝¹ } = { data := data✝ }
rw [h]