Theorem: Array.ext_iff (One.lean)

State before:
α : Type u_1
as bs : Array α
⊢ as = bs ↔ as.data = bs.data
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
as bs : Array α
⊢ as = bs → as.data = bs.data

case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs

State before:
case mp
α : Type u_1
as bs : Array α
⊢ as = bs → as.data = bs.data

case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs
Tactic:
. intro eq
  simp only [eq]
State after:
case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs

State before:
case mpr
α : Type u_1
as bs : Array α
⊢ as.data = bs.data → as = bs
Tactic:
. intro eq
  exact Array.ext' eq
State after:
no goals