-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem idxOf_mem_indexesOf [BEq α] [LawfulBEq α] {xs : List α} (m : x ∈ xs) :
    xs.idxOf x ∈ xs.indexesOf x

Proof state:
case cons
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
⊢ idxOf x (h :: t) ∈ indexesOf x (h :: t)

Tactic:
simp [idxOf_cons, indexesOf_cons, cond_eq_if]

Result:
case cons
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
⊢ (if (h == x) = true then 0 else idxOf x t + 1) ∈
    if (h == x) = true then 0 :: map (fun x => x + 1) (indexesOf x t) else map (fun x => x + 1) (indexesOf x t)

Proof state:
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(x == x) = true
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse.tail
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(h == x) = true
a✝ : Mem x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Tactic:
case tail m =>
  specialize ih m
  simpa

Result:
no goals

Proof state:
case cons.isFalse.head
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(x == x) = true
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

case cons.isFalse.tail
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(h == x) = true
a✝ : Mem x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Tactic:
case _ => simp_all

Result:
case cons.isFalse.tail
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(h == x) = true
a✝ : Mem x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Proof state:
case cons.isTrue
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
w : (h == x) = true
⊢ 0 ∈ 0 :: map (fun x => x + 1) (indexesOf x t)

Tactic:
apply mem_cons_self

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
w : ¬(h == x) = true
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Tactic:
cases m

Result:
case cons.isFalse.head
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(x == x) = true
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

case cons.isFalse.tail
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(h == x) = true
a✝ : Mem x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Proof state:
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
w : ¬(h == x) = true
m : Mem x t
ih : idxOf x t ∈ indexesOf x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
w : ¬(h == x) = true
m : Mem x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Tactic:
specialize ih m

Result:
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
w : ¬(h == x) = true
m : Mem x t
ih : idxOf x t ∈ indexesOf x t
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)

Proof state:
case nil
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
m : x ∈ []
⊢ idxOf x [] ∈ indexesOf x []

Tactic:
simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
⊢ (if (h == x) = true then 0 else idxOf x t + 1) ∈
    if (h == x) = true then 0 :: map (fun x => x + 1) (indexesOf x t) else map (fun x => x + 1) (indexesOf x t)

Tactic:
split <;> rename_i w

Result:
case cons.isTrue
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
w : (h == x) = true
⊢ 0 ∈ 0 :: map (fun x => x + 1) (indexesOf x t)

case cons.isFalse
α : Type u_1
x : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : α
t : List α
ih : x ∈ t → idxOf x t ∈ indexesOf x t
m : x ∈ h :: t
w : ¬(h == x) = true
⊢ idxOf x t + 1 ∈ map (fun x => x + 1) (indexesOf x t)