-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem replace_eq_replaceTR : @List.replace = @replaceTR

Proof state:
⊢ @replace = @replaceTR

Tactic:
funext α _ l b c

Result:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ l.replace b c = l.replaceTR b c

Proof state:
case h.h.h.h.h.nil
α : Type u_1
x✝ : BEq α
l : List α
b c : α
acc : Array α
⊢ l = acc.toList ++ [] → replaceTR.go l b c [] acc = acc.toList ++ [].replace b c

Tactic:
simp [replace, replaceTR.go]

Result:
no goals

Proof state:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ l.replace b c = l.replaceTR b c

Tactic:
simp [replaceTR]

Result:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ l.replace b c = replaceTR.go l b c l #[]

Proof state:
case h.h.h.h.h.cons.h_1
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
x✝ : Bool
heq✝ : (b == x) = true
⊢ l = acc.toList ++ x :: xs →
    (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) = acc.toList ++ c :: xs

Tactic:
simp [*]

Result:
no goals

Proof state:
case h.h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
⊢ l = acc.toList ++ x :: xs → replaceTR.go l b c (x :: xs) acc = acc.toList ++ (x :: xs).replace b c

Tactic:
simp only [replaceTR.go, Array.toListAppend_eq, replace]

Result:
case h.h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
⊢ l = acc.toList ++ x :: xs →
    (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) =
      acc.toList ++
        match b == x with
        | true => c :: xs
        | false => x :: xs.replace b c

Proof state:
case h.h.h.h.h.cons
α : Type u_1
x✝ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
⊢ l = acc.toList ++ x :: xs →
    (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) =
      acc.toList ++
        match b == x with
        | true => c :: xs
        | false => x :: xs.replace b c

Tactic:
split

Result:
case h.h.h.h.h.cons.h_1
α : Type u_1
x✝¹ : BEq α
l : List α
b c x : α
xs : List α
IH : ∀ (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
x✝ : Bool
heq✝ : (b == x) = true
⊢ l = acc.toList ++ x :: xs →
    (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) = acc.toList ++ c :: 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.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
x✝ : Bool
heq✝ : (b == x) = false
⊢ l = acc.toList ++ x :: xs →
    (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) = acc.toList ++ x :: xs.replace b c

Proof state:
α : Type u_1
x✝ : BEq α
l : List α
b c : α
this : ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
⊢ l = #[].toList ++ l

Tactic:
simp

Result:
no goals

Proof state:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ l.replace b c = replaceTR.go l b c l #[]

Tactic:
suffices ∀ xs acc, l = acc.toList ++ xs →
    replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c from
  (this l #[] (by simp)).symm

Result:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c

Proof state:
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.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
x✝ : Bool
heq✝ : (b == x) = false
⊢ l = acc.toList ++ x :: xs →
    (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) = acc.toList ++ x :: xs.replace b c

Tactic:
intro h

Result:
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.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
x✝ : Bool
heq✝ : (b == x) = false
h : l = acc.toList ++ x :: xs
⊢ (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) = acc.toList ++ x :: xs.replace b c

Proof state:
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.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c
acc : Array α
x✝ : Bool
heq✝ : (b == x) = false
h : l = acc.toList ++ x :: xs
⊢ (bif b == x then acc.toList ++ c :: xs else replaceTR.go l b c xs (acc.push x)) = acc.toList ++ x :: xs.replace b c

Tactic:
rw [IH] <;> simp_all

Result:
no goals

Proof state:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
⊢ ∀ (xs : List α) (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c

Tactic:
intro xs

Result:
case h.h.h.h.h
α : Type u_1
x✝ : BEq α
l : List α
b c : α
xs : List α
⊢ ∀ (acc : Array α), l = acc.toList ++ xs → replaceTR.go l b c xs acc = acc.toList ++ xs.replace b c