case nil
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
h : a ∈ []
⊢ indexOf a ([] ++ l₂) = indexOf a []

case cons
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
⊢ indexOf a (d₁ :: t₁ ++ l₂) = indexOf a (d₁ :: t₁)
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h : a ∈ l₁
⊢ indexOf a (l₁ ++ l₂) = indexOf a l₁
induction' l₁ with d₁ t₁ ih
case cons
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
⊢ indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
case cons
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
⊢ indexOf a (d₁ :: t₁ ++ l₂) = indexOf a (d₁ :: t₁)
rw [List.cons_append]
case pos
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
hh : a = d₁
⊢ indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)

case neg
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
hh : ¬a = d₁
⊢ indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
case cons
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
⊢ indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
by_cases hh : a = d₁
no goals
case neg
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
hh : ¬a = d₁
⊢ indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
rw [indexOf_cons_ne _ hh, indexOf_cons_ne _ hh, ih (mem_of_ne_of_mem hh h)]
case nil.h
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
h : a ∈ []
⊢ False
case nil
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
h : a ∈ []
⊢ indexOf a ([] ++ l₂) = indexOf a []
exfalso
no goals
case nil.h
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
h : a ∈ []
⊢ False
exact not_mem_nil a h
no goals
case pos
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
hh : a = d₁
⊢ indexOf a (d₁ :: (t₁ ++ l₂)) = indexOf a (d₁ :: t₁)
iterate 2 rw [indexOf_cons_eq _ hh]
no goals
case pos
ι : Type ?u.81722
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
h✝ : a ∈ l₁
d₁ : α
t₁ : List α
ih : a ∈ t₁ → indexOf a (t₁ ++ l₂) = indexOf a t₁
h : a ∈ d₁ :: t₁
hh : a = d₁
⊢ 0 = indexOf a (d₁ :: t₁)
rw [indexOf_cons_eq _ hh]