-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem takeWhile₂_eq_takeWhile₂TR : @takeWhile₂ = @takeWhile₂TR

Proof state:
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
as : List α
bs : List β
acca : List α
accb : List β
⊢ (match as, bs, acca, accb with
    | a :: as, b :: bs, acca, accb =>
      bif R a b then takeWhile₂TR.go R as bs (a :: acca) (b :: accb) else (acca.reverse, accb.reverse)
    | x, x_1, acca, accb => (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (match as, bs with
          | a :: as, b :: bs =>
            if R a b = true then
              match takeWhile₂ R as bs with
              | (as', bs') => (a :: as', b :: bs')
            else ([], [])
          | x, x_1 => ([], [])).fst,
      accb.reverse ++
        (match as, bs with
          | a :: as, b :: bs =>
            if R a b = true then
              match takeWhile₂ R as bs with
              | (as', bs') => (a :: as', b :: bs')
            else ([], [])
          | x, x_1 => ([], [])).snd)

Tactic:
split <;> simp

Result:
case h_1
α : Type u_2
β : Type u_1
R : α → β → Bool
as : List α
bs : List β
acca : List α
accb : List β
x✝³ : List α
x✝² : List β
x✝¹ : List α
x✝ : List β
a✝ : α
as✝ : List α
b✝ : β
bs✝ : List β
⊢ (bif R a✝ b✝ then takeWhile₂TR.go R as✝ bs✝ (a✝ :: acca) (b✝ :: accb) else (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).fst,
      accb.reverse ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).snd)

Proof state:
⊢ @takeWhile₂ = @takeWhile₂TR

Tactic:
funext α β R as bs

Result:
case h.h.h.h.h
α : Type u_2
β : Type u_1
R : α → β → Bool
as : List α
bs : List β
⊢ takeWhile₂ R as bs = takeWhile₂TR R as bs

Proof state:
case h.h.h.h.h
α : Type u_2
β : Type u_1
R : α → β → Bool
as : List α
bs : List β
⊢ takeWhile₂ R as bs = takeWhile₂TR.go R as bs [] []

Tactic:
exact (go as bs [] []).symm

Result:
no goals

Proof state:
case h_1
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
acca : List α
accb : List β
x✝³ : List α
x✝² : List β
x✝¹ : List α
x✝ : List β
a : α
as : List α
b : β
bs : List β
⊢ (bif R a b then takeWhile₂TR.go R as bs (a :: acca) (b :: accb) else (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      accb.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)

Tactic:
unfold cond

Result:
case h_1
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
acca : List α
accb : List β
x✝³ : List α
x✝² : List β
x✝¹ : List α
x✝ : List β
a : α
as : List α
b : β
bs : List β
⊢ (match R a b with
    | true => takeWhile₂TR.go R as bs (a :: acca) (b :: accb)
    | false => (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      accb.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)

Proof state:
case h_1
α : Type u_2
β : Type u_1
R : α → β → Bool
as : List α
bs : List β
acca : List α
accb : List β
x✝³ : List α
x✝² : List β
x✝¹ : List α
x✝ : List β
a✝ : α
as✝ : List α
b✝ : β
bs✝ : List β
⊢ (bif R a✝ b✝ then takeWhile₂TR.go R as✝ bs✝ (a✝ :: acca) (b✝ :: accb) else (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).fst,
      accb.reverse ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).snd)

Tactic:
rename_i a as b bs

Result:
case h_1
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
acca : List α
accb : List β
x✝³ : List α
x✝² : List β
x✝¹ : List α
x✝ : List β
a : α
as : List α
b : β
bs : List β
⊢ (bif R a b then takeWhile₂TR.go R as bs (a :: acca) (b :: accb) else (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      accb.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)

Proof state:
case h.h.h.h.h
α : Type u_2
β : Type u_1
R : α → β → Bool
as : List α
bs : List β
⊢ takeWhile₂ R as bs = takeWhile₂TR R as bs

Tactic:
simp [takeWhile₂TR]

Result:
case h.h.h.h.h
α : Type u_2
β : Type u_1
R : α → β → Bool
as : List α
bs : List β
⊢ takeWhile₂ R as bs = takeWhile₂TR.go R as bs [] []

Proof state:
case h_1
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
acca : List α
accb : List β
x✝³ : List α
x✝² : List β
x✝¹ : List α
x✝ : List β
a : α
as : List α
b : β
bs : List β
⊢ (match R a b with
    | true => takeWhile₂TR.go R as bs (a :: acca) (b :: accb)
    | false => (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      accb.reverse ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)

Tactic:
cases R a b <;> simp [go as bs]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
as : List α
bs : List β
acca : List α
accb : List β
⊢ takeWhile₂TR.go R as bs acca accb =
    (acca.reverse ++ (takeWhile₂ R as bs).fst, accb.reverse ++ (takeWhile₂ R as bs).snd)

Tactic:
unfold takeWhile₂TR.go takeWhile₂

Result:
α : Type u_2
β : Type u_1
R : α → β → Bool
as✝ : List α
bs✝ : List β
as : List α
bs : List β
acca : List α
accb : List β
⊢ (match as, bs, acca, accb with
    | a :: as, b :: bs, acca, accb =>
      bif R a b then takeWhile₂TR.go R as bs (a :: acca) (b :: accb) else (acca.reverse, accb.reverse)
    | x, x_1, acca, accb => (acca.reverse, accb.reverse)) =
    (acca.reverse ++
        (match as, bs with
          | a :: as, b :: bs =>
            if R a b = true then
              match takeWhile₂ R as bs with
              | (as', bs') => (a :: as', b :: bs')
            else ([], [])
          | x, x_1 => ([], [])).fst,
      accb.reverse ++
        (match as, bs with
          | a :: as, b :: bs =>
            if R a b = true then
              match takeWhile₂ R as bs with
              | (as', bs') => (a :: as', b :: bs')
            else ([], [])
          | x, x_1 => ([], [])).snd)