case nil
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ indexOf a [] ≤ length []

case cons
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
⊢ indexOf a (b :: l) ≤ length (b :: l)
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
⊢ indexOf a l ≤ length l
induction' l with b l ih
case cons
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
⊢ (if a = b then 0 else succ (indexOf a l)) ≤ length l + 1
case cons
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
⊢ indexOf a (b :: l) ≤ length (b :: l)
simp only [length, indexOf_cons]
case pos
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : a = b
⊢ (if a = b then 0 else succ (indexOf a l)) ≤ length l + 1

case neg
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : ¬a = b
⊢ (if a = b then 0 else succ (indexOf a l)) ≤ length l + 1
case cons
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
⊢ (if a = b then 0 else succ (indexOf a l)) ≤ length l + 1
by_cases h : a = b
case neg
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : ¬a = b
⊢ succ (indexOf a l) ≤ length l + 1
case neg
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : ¬a = b
⊢ (if a = b then 0 else succ (indexOf a l)) ≤ length l + 1
rw [if_neg h]
no goals
case neg
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : ¬a = b
⊢ succ (indexOf a l) ≤ length l + 1
exact succ_le_succ ih
no goals
case nil
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ indexOf a [] ≤ length []
rfl
case pos
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : a = b
⊢ 0 ≤ length l + 1
case pos
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : a = b
⊢ (if a = b then 0 else succ (indexOf a l)) ≤ length l + 1
rw [if_pos h]
no goals
case pos
ι : Type ?u.80422
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l ≤ length l
h : a = b
⊢ 0 ≤ length l + 1
exact Nat.zero_le _