case a
α : Type u_1
as bs : List α
⊢ toArray as = toArray bs ↔ as = bs
α : Type u_1
as bs : List α
⊢ (toArray as = toArray bs) = (as = bs)
apply propext
case a.mp
α : Type u_1
as bs : List α
⊢ toArray as = toArray bs → as = bs

case a.mpr
α : Type u_1
as bs : List α
⊢ as = bs → toArray as = toArray bs
case a
α : Type u_1
as bs : List α
⊢ toArray as = toArray bs ↔ as = bs
apply Iff.intro
case a.mp
α : Type u_1
as bs : List α
h : toArray as = toArray bs
⊢ as = bs
case a.mp
α : Type u_1
as bs : List α
⊢ toArray as = toArray bs → as = bs
intro h
case a.mp
α : Type u_1
as bs : List α
h : toArrayAux as (Array.mkEmpty (redLength as)) = toArrayAux bs (Array.mkEmpty (redLength bs))
⊢ as = bs
case a.mp
α : Type u_1
as bs : List α
h : toArray as = toArray bs
⊢ as = bs
simp [toArray] at h
case a.mp
α : Type u_1
as bs : List α
h : toArrayAux as (Array.mkEmpty (redLength as)) = toArrayAux bs (Array.mkEmpty (redLength bs))
this : as = bs ∧ Array.mkEmpty (redLength as) = Array.mkEmpty (redLength bs)
⊢ as = bs
case a.mp
α : Type u_1
as bs : List α
h : toArrayAux as (Array.mkEmpty (redLength as)) = toArrayAux bs (Array.mkEmpty (redLength bs))
⊢ as = bs
have := of_toArrayAux_eq_toArrayAux h rfl
no goals
case a.mp
α : Type u_1
as bs : List α
h : toArrayAux as (Array.mkEmpty (redLength as)) = toArrayAux bs (Array.mkEmpty (redLength bs))
this : as = bs ∧ Array.mkEmpty (redLength as) = Array.mkEmpty (redLength bs)
⊢ as = bs
exact this.1
case a.mpr
α : Type u_1
as bs : List α
h : as = bs
⊢ toArray as = toArray bs
case a.mpr
α : Type u_1
as bs : List α
⊢ as = bs → toArray as = toArray bs
intro h
no goals
case a.mpr
α : Type u_1
as bs : List α
h : as = bs
⊢ toArray as = toArray bs
rw [h]