case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ replace l b c = replaceTR l b c
⊢ @replace = @replaceTR
funext α _ l b c
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ replace l b c = replaceTR.go l b c l #[]
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ replace l b c = replaceTR l b c
simp [replaceTR]
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ replace l b c = replaceTR.go l b c l #[]
suffices ∀ xs acc, l = acc.data ++ xs →
    replaceTR.go l b c xs acc = acc.data ++ xs.replace b c from
  (this l #[] (by simp)).symm
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
xs : List α
⊢ ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
intro xs
no goals
α : Type u_1
x✝ : BEq α
l : List α
b c : α
this : ∀ (xs : List α) (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
⊢ l = #[].data ++ l
simp
no goals
case h.h.h.h.h.nil
α : Type u_1
x✝ : BEq α
l : List α
b c : α
acc : Array α
⊢ l = acc.data ++ [] → replaceTR.go l b c [] acc = acc.data ++ replace [] b c
simp [replace, replaceTR.go]
case h.h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
⊢ l = acc.data ++ x :: xs →
    (bif x == b then acc.data ++ c :: xs else replaceTR.go l b c xs (Array.push acc x)) =
      acc.data ++
        match x == b with
        | true => c :: xs
        | false => x :: replace xs b c
case h.h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
⊢ l = acc.data ++ x :: xs → replaceTR.go l b c (x :: xs) acc = acc.data ++ replace (x :: xs) b c
simp [replace, replaceTR.go]
case h.h.h.h.h.cons.h_2
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
⊢ l = acc.data ++ x :: xs → replaceTR.go l b c xs (Array.push acc x) = acc.data ++ x :: replace xs b c
case h.h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
⊢ l = acc.data ++ x :: xs →
    (bif x == b then acc.data ++ c :: xs else replaceTR.go l b c xs (Array.push acc x)) =
      acc.data ++
        match x == b with
        | true => c :: xs
        | false => x :: replace xs b c
split <;> simp [*]
case h.h.h.h.h.cons.h_2
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ replaceTR.go l b c xs (Array.push acc x) = acc.data ++ x :: replace xs b c
case h.h.h.h.h.cons.h_2
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
⊢ l = acc.data ++ x :: xs → replaceTR.go l b c xs (Array.push acc x) = acc.data ++ x :: replace xs b c
intro h
case h.h.h.h.h.cons.h_2
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ replace xs b c = acc.data ++ x :: replace xs b c

case h.h.h.h.h.cons.h_2.a
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case h.h.h.h.h.cons.h_2
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ replaceTR.go l b c xs (Array.push acc x) = acc.data ++ x :: replace xs b c
rw [IH]
case h.h.h.h.h.cons.h_2.a
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
case h.h.h.h.h.cons.h_2
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ (Array.push acc x).data ++ replace xs b c = acc.data ++ x :: replace xs b c

case h.h.h.h.h.cons.h_2.a
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp
case h.h.h.h.h.cons.h_2.a
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ l = acc.data ++ x :: xs
case h.h.h.h.h.cons.h_2.a
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ l = (Array.push acc x).data ++ xs
simp
no goals
case h.h.h.h.h.cons.h_2.a
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.data ++ xs → replaceTR.go l b c xs acc = acc.data ++ replace xs b c
acc : Array α
x✝ : Bool
heq✝ : (x == b) = false
h : l = acc.data ++ x :: xs
⊢ l = acc.data ++ x :: xs
exact h