-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/BasicAux.lean
theorem List.of_toArrayAux_eq_toArrayAux {as bs : List α} {cs ds : Array α} (h : as.toArrayAux cs = bs.toArrayAux ds) (hlen : cs.size = ds.size) : as = bs ∧ cs = ds

Proof state:
α : Type u_1
as bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
b : α
bs : List α
h : cs = bs.toArrayAux (ds.push b)
⊢ [] = b :: bs ∧ cs = ds

Tactic:
rw [h] at hlen

Result:
α : Type u_1
as bs✝ : List α
cs ds : Array α
b : α
bs : List α
hlen : (bs.toArrayAux (ds.push b)).size = ds.size
h : cs = bs.toArrayAux (ds.push b)
⊢ [] = b :: bs ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this✝ : (cs.push a).size = (ds.push b).size
ih₁ : as = bs
ih₂ : cs.push a = ds.push b
this : cs = ds ∧ a = b
⊢ a = b ∧ cs = ds

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type u_1
as bs : List α
cs ds : Array α
hlen : cs.size = ds.size
h : cs = ds
⊢ [] = [] ∧ cs = ds

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
as bs✝ : List α
cs ds : Array α
b : α
bs : List α
hlen : (bs.toArrayAux (ds.push b)).size = ds.size
h : cs = bs.toArrayAux (ds.push b)
⊢ [] = b :: bs ∧ cs = ds

Tactic:
simp_arith [size_toArrayAux] at hlen

Result:
no goals

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
⊢ (cs.push a).size = (ds.push b).size

Tactic:
simp [*]

Result:
no goals

Proof state:
α : Type u_1
as bs : List α
cs ds : Array α
hlen : cs.size = ds.size
h : [].toArrayAux cs = [].toArrayAux ds
⊢ [] = [] ∧ cs = ds

Tactic:
simp [toArrayAux] at h

Result:
α : Type u_1
as bs : List α
cs ds : Array α
hlen : cs.size = ds.size
h : cs = ds
⊢ [] = [] ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this : (cs.push a).size = (ds.push b).size
ih₁ : as = bs
ih₂ : cs.push a = ds.push b
⊢ a = b ∧ cs = ds

Tactic:
have := Array.of_push_eq_push ih₂

Result:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this✝ : (cs.push a).size = (ds.push b).size
ih₁ : as = bs
ih₂ : cs.push a = ds.push b
this : cs = ds ∧ a = b
⊢ a = b ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
h : as.toArrayAux (cs.push a) = ds
⊢ a :: as = [] ∧ cs = ds

Tactic:
rw [← h] at hlen

Result:
α : Type u_1
as✝ bs : List α
cs ds : Array α
a : α
as : List α
hlen : cs.size = (as.toArrayAux (cs.push a)).size
h : as.toArrayAux (cs.push a) = ds
⊢ a :: as = [] ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
h : (a :: as).toArrayAux cs = [].toArrayAux ds
⊢ a :: as = [] ∧ cs = ds

Tactic:
simp [toArrayAux] at h

Result:
α : Type u_1
as✝ bs : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
h : as.toArrayAux (cs.push a) = ds
⊢ a :: as = [] ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs : List α
cs ds : Array α
a : α
as : List α
hlen : cs.size = (as.toArrayAux (cs.push a)).size
h : as.toArrayAux (cs.push a) = ds
⊢ a :: as = [] ∧ cs = ds

Tactic:
simp_arith [size_toArrayAux] at hlen

Result:
no goals

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this : (cs.push a).size = (ds.push b).size
ih₁ : as = bs
ih₂ : cs.push a = ds.push b
⊢ a :: as = b :: bs ∧ cs = ds

Tactic:
simp [ih₁]

Result:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this : (cs.push a).size = (ds.push b).size
ih₁ : as = bs
ih₂ : cs.push a = ds.push b
⊢ a = b ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : (a :: as).toArrayAux cs = (b :: bs).toArrayAux ds
⊢ a :: as = b :: bs ∧ cs = ds

Tactic:
simp [toArrayAux] at h

Result:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
⊢ a :: as = b :: bs ∧ cs = ds

Proof state:
α : Type u_1
as bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
b : α
bs : List α
h : [].toArrayAux cs = (b :: bs).toArrayAux ds
⊢ [] = b :: bs ∧ cs = ds

Tactic:
simp [toArrayAux] at h

Result:
α : Type u_1
as bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
b : α
bs : List α
h : cs = bs.toArrayAux (ds.push b)
⊢ [] = b :: bs ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this : (cs.push a).size = (ds.push b).size
⊢ a :: as = b :: bs ∧ cs = ds

Tactic:
have ⟨ih₁, ih₂⟩ := of_toArrayAux_eq_toArrayAux h this

Result:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this : (cs.push a).size = (ds.push b).size
ih₁ : as = bs
ih₂ : cs.push a = ds.push b
⊢ a :: as = b :: bs ∧ cs = ds

Proof state:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
⊢ a :: as = b :: bs ∧ cs = ds

Tactic:
have : (cs.push a).size = (ds.push b).size := by simp [*]

Result:
α : Type u_1
as✝ bs✝ : List α
cs ds : Array α
hlen : cs.size = ds.size
a : α
as : List α
b : α
bs : List α
h : as.toArrayAux (cs.push a) = bs.toArrayAux (ds.push b)
this : (cs.push a).size = (ds.push b).size
⊢ a :: as = b :: bs ∧ cs = ds

Proof state:
α : Type u_1
as bs : List α
cs ds : Array α
h : as.toArrayAux cs = bs.toArrayAux ds
hlen : cs.size = ds.size
⊢ as = bs ∧ cs = ds

Tactic:
match as, bs with
| [], []    => simp [toArrayAux] at h; simp [h]
| a::as, [] => simp [toArrayAux] at h; rw [← h] at hlen; simp_arith [size_toArrayAux] at hlen
| [], b::bs => simp [toArrayAux] at h; rw [h] at hlen; simp_arith [size_toArrayAux] at hlen
| a::as, b::bs =>
  simp [toArrayAux] at h
  have : (cs.push a).size = (ds.push b).size := by simp [*]
  have ⟨ih₁, ih₂⟩ := of_toArrayAux_eq_toArrayAux h this
  simp [ih₁]
  have := Array.of_push_eq_push ih₂
  simp [this]

Result:
no goals