-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem replace_takeWhile [BEq α] [LawfulBEq α] {l : List α} {p : α → Bool} (h : p a = p b) :
    (l.takeWhile p).replace a b = (l.replace a b).takeWhile p

Proof state:
case cons.isTrue.h_1
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : p x = true
x✝ : Bool
h₂ : (a == x) = true
⊢ (x :: takeWhile p xs).replace a b = takeWhile p (b :: xs)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse.h_1
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : ¬p x = true
x✝ : Bool
h₂ : (a == x) = true
⊢ [].replace a b = takeWhile p (b :: xs)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
⊢ (if p x = true then x :: takeWhile p xs else []).replace a b =
    takeWhile p
      (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b)

Tactic:
split <;> rename_i h₁ <;> split <;> rename_i h₂

Result:
case cons.isTrue.h_1
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : p x = true
x✝ : Bool
h₂ : (a == x) = true
⊢ (x :: takeWhile p xs).replace a b = takeWhile p (b :: xs)

case cons.isTrue.h_2
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : p x = true
x✝ : Bool
h₂ : (a == x) = false
⊢ (x :: takeWhile p xs).replace a b = takeWhile p (x :: xs.replace a b)

case cons.isFalse.h_1
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : ¬p x = true
x✝ : Bool
h₂ : (a == x) = true
⊢ [].replace a b = takeWhile p (b :: xs)

case cons.isFalse.h_2
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : ¬p x = true
x✝ : Bool
h₂ : (a == x) = false
⊢ [].replace a b = takeWhile p (x :: xs.replace a b)

Proof state:
case nil
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
⊢ (takeWhile p []).replace a b = takeWhile p ([].replace a b)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
⊢ (takeWhile p (x :: xs)).replace a b = takeWhile p ((x :: xs).replace a b)

Tactic:
simp only [takeWhile_cons, replace_cons]

Result:
case cons
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
⊢ (if p x = true then x :: takeWhile p xs else []).replace a b =
    takeWhile p
      (match a == x with
      | true => b :: xs
      | false => x :: xs.replace a b)

Proof state:
case cons.isTrue.h_2
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : p x = true
x✝ : Bool
h₂ : (a == x) = false
⊢ (x :: takeWhile p xs).replace a b = takeWhile p (x :: xs.replace a b)

Tactic:
simp [replace_cons, h₂, takeWhile_cons, h₁, ih]

Result:
no goals

Proof state:
case cons.isFalse.h_2
α : Type u_1
a b : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
h : p a = p b
x : α
xs : List α
ih : (takeWhile p xs).replace a b = takeWhile p (xs.replace a b)
h₁ : ¬p x = true
x✝ : Bool
h₂ : (a == x) = false
⊢ [].replace a b = takeWhile p (x :: xs.replace a b)

Tactic:
simp_all

Result:
no goals