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

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

case cons.inr
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : ¬a = b
⊢ succ (indexOf a l) = length l + 1 ↔ ¬(a = b ∨ a ∈ l)
case cons
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
⊢ (if a = b then 0 else succ (indexOf a l)) = length l + 1 ↔ ¬(a = b ∨ a ∈ l)
split_ifs with h
no goals
case nil
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ indexOf a [] = length [] ↔ ¬a ∈ []
exact iff_of_true rfl (not_mem_nil _)
no goals
case cons.inl
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : a = b
⊢ 0 = length l + 1 ↔ ¬(a = b ∨ a ∈ l)
exact iff_of_false (by rintro ⟨⟩) fun H => H <| Or.inl h
no goals
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : a = b
⊢ ¬0 = length l + 1
rintro ⟨⟩
case cons.inr
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : ¬a = b
⊢ succ (indexOf a l) = length l + 1 ↔ ¬a ∈ l
case cons.inr
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : ¬a = b
⊢ succ (indexOf a l) = length l + 1 ↔ ¬(a = b ∨ a ∈ l)
simp only [h, false_or_iff]
case cons.inr
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : ¬a = b
⊢ succ (indexOf a l) = length l + 1 ↔ indexOf a l = length l
case cons.inr
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : ¬a = b
⊢ succ (indexOf a l) = length l + 1 ↔ ¬a ∈ l
rw [← ih]
no goals
case cons.inr
ι : Type ?u.79233
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a b : α
l : List α
ih : indexOf a l = length l ↔ ¬a ∈ l
h : ¬a = b
⊢ succ (indexOf a l) = length l + 1 ↔ indexOf a l = length l
exact succ_inj'