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
⊢ @takeWhile₂ = @takeWhile₂TR
funext α β R as bs
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 [] []
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
simp [takeWhile₂TR]
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 [] []
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 [] []
let rec go (as bs acca accb) : takeWhile₂TR.go R as bs acca accb =
    (acca.reverse ++ (as.takeWhile₂ R bs).1, accb.reverse ++ (as.takeWhile₂ R bs).2) := by
  unfold takeWhile₂TR.go takeWhile₂; split <;> simp
  rename_i a as b bs; unfold cond; cases R a b <;> simp [go as bs]
no goals
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 [] []
exact (go as bs [] []).symm
α : 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 (reverse acca, reverse accb)
    | x, x_1, acca, accb => (reverse acca, reverse accb)) =
    (reverse acca ++
        (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,
      reverse accb ++
        (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)
α : 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 =
    (reverse acca ++ (takeWhile₂ R as bs).fst, reverse accb ++ (takeWhile₂ R as bs).snd)
unfold takeWhile₂TR.go takeWhile₂
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 (reverse acca, reverse accb)) =
    (reverse acca ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).fst,
      reverse accb ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).snd)
α : 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 (reverse acca, reverse accb)
    | x, x_1, acca, accb => (reverse acca, reverse accb)) =
    (reverse acca ++
        (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,
      reverse accb ++
        (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)
split <;> simp
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 (reverse acca, reverse accb)) =
    (reverse acca ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      reverse accb ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)
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 (reverse acca, reverse accb)) =
    (reverse acca ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).fst,
      reverse accb ++
        (if R a✝ b✝ = true then (a✝ :: (takeWhile₂ R as✝ bs✝).fst, b✝ :: (takeWhile₂ R as✝ bs✝).snd) else ([], [])).snd)
rename_i a as b bs
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 => (reverse acca, reverse accb)) =
    (reverse acca ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      reverse accb ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)
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 (reverse acca, reverse accb)) =
    (reverse acca ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      reverse accb ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)
unfold cond
no goals
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 => (reverse acca, reverse accb)) =
    (reverse acca ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).fst,
      reverse accb ++
        (if R a b = true then (a :: (takeWhile₂ R as bs).fst, b :: (takeWhile₂ R as bs).snd) else ([], [])).snd)
cases R a b <;> simp [go as bs]