-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_some_iff_findIdx_eq {xs : List α} {p : α → Bool} {i : Nat} :
    xs.findIdx? p = some i ↔ i < xs.length ∧ xs.findIdx p = i

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = true
⊢ 0 = i → i < xs.length + 1

Tactic:
rintro rfl

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = true
⊢ 0 < xs.length + 1

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
⊢ findIdx? p (x :: xs) = some i ↔ i < (x :: xs).length ∧ findIdx p (x :: xs) = i

Tactic:
simp only [findIdx?_cons, findIdx_cons]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = some i ↔
    i < (x :: xs).length ∧ (bif p x then 0 else findIdx p xs + 1) = i

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p xs) = some i ↔
    i < (x :: xs).length ∧ (bif p x then 0 else findIdx p xs + 1) = i

Tactic:
simp_all [cond_eq_if, and_assoc]

Result:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = false
⊢ (∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = i) ↔ i < xs.length + 1 ∧ findIdx p xs + 1 = i

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) = some i ↔
    i < (x :: xs).length ∧ (bif p x then 0 else findIdx p xs + 1) = i

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = true
⊢ some 0 = some i ↔ i < (x :: xs).length ∧ (bif p x then 0 else findIdx p xs + 1) = i

case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p xs) = some i ↔
    i < (x :: xs).length ∧ (bif p x then 0 else findIdx p xs + 1) = i

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = false
h : findIdx p xs + 1 < xs.length + 1
⊢ findIdx p xs < xs.length

Tactic:
simp_all [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons.isFalse.mpr.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = false
h : findIdx p xs + 1 < xs.length + 1
⊢ ∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = findIdx p xs + 1

Tactic:
exact ⟨_, by simp_all [Nat.succ_lt_succ_iff], rfl, rfl⟩

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
i : Nat
⊢ findIdx? p [] = some i ↔ i < [].length ∧ findIdx p [] = i

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = false
⊢ (∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = i) ↔ i < xs.length + 1 ∧ findIdx p xs + 1 = i

Tactic:
constructor

Result:
case cons.isFalse.mp
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = false
⊢ (∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = i) → i < xs.length + 1 ∧ findIdx p xs + 1 = i

case cons.isFalse.mpr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = false
⊢ i < xs.length + 1 ∧ findIdx p xs + 1 = i → ∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = i

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = true
⊢ 0 < xs.length + 1

Tactic:
exact zero_lt_succ xs.length

Result:
no goals

Proof state:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = true
⊢ some 0 = some i ↔ i < (x :: xs).length ∧ (bif p x then 0 else findIdx p xs + 1) = i

Tactic:
simp_all [cond_eq_if]

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = true
⊢ 0 = i → i < xs.length + 1

Proof state:
case cons.isFalse.mp
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = false
⊢ (∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = i) → i < xs.length + 1 ∧ findIdx p xs + 1 = i

Tactic:
rintro ⟨a, lt, rfl, rfl⟩

Result:
case cons.isFalse.mp.intro.intro.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = false
lt : findIdx p xs < xs.length
⊢ findIdx p xs + 1 < xs.length + 1 ∧ findIdx p xs + 1 = findIdx p xs + 1

Proof state:
case cons.isFalse.mpr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
i : Nat
h✝ : p x = false
⊢ i < xs.length + 1 ∧ findIdx p xs + 1 = i → ∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = i

Tactic:
rintro ⟨h, rfl⟩

Result:
case cons.isFalse.mpr.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = false
h : findIdx p xs + 1 < xs.length + 1
⊢ ∃ a, a < xs.length ∧ findIdx p xs = a ∧ a + 1 = findIdx p xs + 1

Proof state:
case cons.isFalse.mp.intro.intro.intro
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ i < xs.length ∧ findIdx p xs = i
h✝ : p x = false
lt : findIdx p xs < xs.length
⊢ findIdx p xs + 1 < xs.length + 1 ∧ findIdx p xs + 1 = findIdx p xs + 1

Tactic:
simp_all [Nat.succ_lt_succ_iff]

Result:
no goals