-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf_lt_length [BEq α] [LawfulBEq α] {l : List α} (h : a ∈ l) : l.idxOf a < l.length

Proof state:
case cons.inr
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a ∈ xs
⊢ idxOf a (x :: xs) < (x :: xs).length

Tactic:
simp only [idxOf_cons, cond_eq_if, beq_iff_eq, length_cons]

Result:
case cons.inr
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a ∈ xs
⊢ (if (x == a) = true then 0 else idxOf a xs + 1) < xs.length + 1

Proof state:
case cons.inr.isTrue
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
h : a ∈ xs
ih : idxOf a xs < xs.length
h✝ : (x == a) = true
⊢ 0 < xs.length + 1

Tactic:
exact zero_lt_succ xs.length

Result:
no goals

Proof state:
case cons.inr.isFalse
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
h : a ∈ xs
ih : idxOf a xs < xs.length
h✝ : ¬(x == a) = true
⊢ idxOf a xs + 1 < xs.length + 1

Tactic:
exact Nat.add_lt_add_right ih 1

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a = x ∨ a ∈ xs
⊢ idxOf a (x :: xs) < (x :: xs).length

Tactic:
obtain rfl | h := h

Result:
case cons.inl
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
⊢ idxOf a (a :: xs) < (a :: xs).length

case cons.inr
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a ∈ xs
⊢ idxOf a (x :: xs) < (x :: xs).length

Proof state:
case cons.inr
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
h : a ∈ xs
ih : idxOf a xs < xs.length
⊢ (if (x == a) = true then 0 else idxOf a xs + 1) < xs.length + 1

Tactic:
split

Result:
case cons.inr.isTrue
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
h : a ∈ xs
ih : idxOf a xs < xs.length
h✝ : (x == a) = true
⊢ 0 < xs.length + 1

case cons.inr.isFalse
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
h : a ∈ xs
ih : idxOf a xs < xs.length
h✝ : ¬(x == a) = true
⊢ idxOf a xs + 1 < xs.length + 1

Proof state:
case cons.inl
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
⊢ idxOf a (a :: xs) < (a :: xs).length

Tactic:
simp

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a ∈ xs
⊢ (if (x == a) = true then 0 else idxOf a xs + 1) < xs.length + 1

Tactic:
specialize ih h

Result:
case cons.inr
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
h : a ∈ xs
ih : idxOf a xs < xs.length
⊢ (if (x == a) = true then 0 else idxOf a xs + 1) < xs.length + 1

Proof state:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a ∈ x :: xs
⊢ idxOf a (x :: xs) < (x :: xs).length

Tactic:
simp only [mem_cons] at h

Result:
case cons
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
xs : List α
ih : a ∈ xs → idxOf a xs < xs.length
h : a = x ∨ a ∈ xs
⊢ idxOf a (x :: xs) < (x :: xs).length

Proof state:
case nil
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : a ∈ []
⊢ idxOf a [] < [].length

Tactic:
simp at h

Result:
no goals