-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findIdx?_eq_some_iff_getElem {xs : List α} {p : α → Bool} {i : Nat} :
    xs.findIdx? p = some i ↔
      ∃ h : i < xs.length, p xs[i] ∧ ∀ j (hji : j < i), ¬p (xs[j]'(Nat.lt_trans hji h))

Proof state:
case cons.isTrue.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : p x = true
i : Nat
x✝ : i + 1 < xs.length + 1
a✝ : p xs[i] = true
⊢ ∃ x_1 h, p (x :: xs)[x_1] = true

Tactic:
refine ⟨0, zero_lt_succ i, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : ¬p x = true
a : Nat
h : a < xs.length
h₁ : p xs[a] = true
h₂ : ∀ (j : Nat) (hji : j < a), p xs[j] = false
⊢ p (x :: xs)[a + 1] = true

Tactic:
simpa

Result:
no goals

Proof state:
case cons.isTrue.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : p x = true
⊢ 0 = 0 ↔ ∃ h, p (x :: xs)[0] = true ∧ ∀ (j : Nat) (hji : j < 0), p (x :: xs)[j] = false

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse.mpr.intro.intro.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : ¬p x = true
i : Nat
h : i + 1 < xs.length + 1
h₁ : p (x :: xs)[i + 1] = true
h₂ : ∀ (j : Nat) (hji : j < i + 1), p (x :: xs)[j] = false
⊢ ∃ a, (∃ h, p xs[a] = true ∧ ∀ (j : Nat) (hji : j < a), p xs[j] = false) ∧ a + 1 = i + 1

Tactic:
refine ⟨i, ⟨Nat.succ_lt_succ_iff.mp h, by simpa, fun j hj => ?_⟩, rfl⟩

Result:
case cons.isFalse.mpr.intro.intro.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : ¬p x = true
i : Nat
h : i + 1 < xs.length + 1
h₁ : p (x :: xs)[i + 1] = true
h₂ : ∀ (j : Nat) (hji : j < i + 1), p (x :: xs)[j] = false
j : Nat
hj : j < i
⊢ p xs[j] = false

Proof state:
case cons.isFalse.mpr.intro.intro.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : ¬p x = true
h : 0 < xs.length + 1
h₁ : p (x :: xs)[0] = true
h₂ : ∀ (j : Nat) (hji : j < 0), p (x :: xs)[j] = false
⊢ ∃ a, (∃ h, p xs[a] = true ∧ ∀ (j : Nat) (hji : j < a), p xs[j] = false) ∧ a + 1 = 0

Tactic:
simp_all

Result:
no goals

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

Tactic:
cases i with
| zero => simp_all
| succ i =>
  refine ⟨i, ⟨Nat.succ_lt_succ_iff.mp h, by simpa, fun j hj => ?_⟩, rfl⟩
  simpa using h₂ (j + 1) (Nat.succ_lt_succ_iff.mpr hj)

Result:
no goals

Proof state:
case cons.isTrue.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : p x = true
i : Nat
⊢ 0 = i + 1 ↔ ∃ h, p (x :: xs)[i + 1] = true ∧ ∀ (j : Nat) (hji : j < i + 1), p (x :: xs)[j] = false

Tactic:
simp only [Bool.not_eq_true, zero_ne_add_one, getElem_cons_succ, false_iff, not_exists,
  not_and, Classical.not_forall, Bool.not_eq_false]

Result:
case cons.isTrue.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : p x = true
i : Nat
⊢ ∀ (x_1 : i + 1 < xs.length + 1), p xs[i] = true → ∃ x_2 h, p (x :: xs)[x_2] = true

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

Tactic:
split

Result:
case cons.isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
i : Nat
h✝ : p x = true
⊢ some 0 = some i ↔ ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p (x :: xs)[j] = true

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

Proof state:
case cons.isTrue.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : p x = true
i : Nat
⊢ ∀ (x_1 : i + 1 < xs.length + 1), p xs[i] = true → ∃ x_2 h, p (x :: xs)[x_2] = true

Tactic:
intros

Result:
case cons.isTrue.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : p x = true
i : Nat
x✝ : i + 1 < xs.length + 1
a✝ : p xs[i] = true
⊢ ∃ x_1 h, p (x :: xs)[x_1] = true

Proof state:
case cons.isFalse.mp.intro.intro.intro.intro.zero
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : ¬p x = true
a : Nat
h : a < xs.length
h₁ : p xs[a] = true
h₂ : ∀ (j : Nat) (hji : j < a), p xs[j] = false
hj : 0 < a + 1
⊢ p (x :: xs)[0] = false

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.isFalse.mpr.intro.intro.succ
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat}, findIdx? p xs = some i ↔ ∃ h, p xs[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p xs[j] = true
h✝ : ¬p x = true
i : Nat
h : i + 1 < xs.length + 1
h₁ : p (x :: xs)[i + 1] = true
h₂ : ∀ (j : Nat) (hji : j < i + 1), p (x :: xs)[j] = false
j : Nat
hj : j < i
⊢ p xs[j] = false

Tactic:
simpa using h₂ (j + 1) (Nat.succ_lt_succ_iff.mpr hj)

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
i : Nat
⊢ findIdx? p [] = some i ↔ ∃ h, p [][i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p [][j] = true

Tactic:
simp

Result:
no goals

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

Tactic:
refine ⟨Nat.succ_lt_succ_iff.mpr h, by simpa, fun j hj => ?_⟩

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