no goals
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p : α → Bool
b : α
l : List α
⊢ findIdx p (b :: l) = bif p b then 0 else findIdx p l + 1
cases H : p b with
  | true => simp [H, findIdx, findIdx.go]
  | false => simp [H, findIdx, findIdx.go, findIdx_go_succ]
no goals
case true
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p : α → Bool
b : α
l : List α
H : p b = true
⊢ findIdx p (b :: l) = bif true then 0 else findIdx p l + 1
simp [H, findIdx, findIdx.go]
no goals
case false
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p : α → Bool
b : α
l : List α
H : p b = false
⊢ findIdx p (b :: l) = bif false then 0 else findIdx p l + 1
simp [H, findIdx, findIdx.go, findIdx_go_succ]
no goals
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l✝ : List α
p : α → Bool
l : List α
n : ℕ
⊢ findIdx.go p l (n + 1) = findIdx.go p l n + 1
cases l with
| nil => unfold List.findIdx.go; exact Nat.succ_eq_add_one n
| cons head tail =>
  unfold List.findIdx.go
  cases p head <;> simp only [cond_false, cond_true]
  exact findIdx_go_succ p tail (n + 1)
case nil
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
⊢ n + 1 = n + 1
case nil
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
⊢ findIdx.go p [] (n + 1) = findIdx.go p [] n + 1
unfold List.findIdx.go
no goals
case nil
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
⊢ n + 1 = n + 1
exact Nat.succ_eq_add_one n
case cons
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
head : α
tail : List α
⊢ (bif p head then n + 1 else findIdx.go p tail (n + 1 + 1)) = (bif p head then n else findIdx.go p tail (n + 1)) + 1
case cons
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
head : α
tail : List α
⊢ findIdx.go p (head :: tail) (n + 1) = findIdx.go p (head :: tail) n + 1
unfold List.findIdx.go
case cons.false
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
head : α
tail : List α
⊢ findIdx.go p tail (n + 1 + 1) = findIdx.go p tail (n + 1) + 1
case cons
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
head : α
tail : List α
⊢ (bif p head then n + 1 else findIdx.go p tail (n + 1 + 1)) = (bif p head then n else findIdx.go p tail (n + 1)) + 1
cases p head <;> simp only [cond_false, cond_true]
no goals
case cons.false
ι : Type ?u.75547
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
p✝ : α → Bool
b : α
l : List α
p : α → Bool
n : ℕ
head : α
tail : List α
⊢ findIdx.go p tail (n + 1 + 1) = findIdx.go p tail (n + 1) + 1
exact findIdx_go_succ p tail (n + 1)