-- 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.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

Tactic:
simp only [Option.map_eq_some', ih, Bool.not_eq_true, length_cons]

Result:
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
⊢ (∃ a, (∃ h, p xs[a] = true ∧ ∀ (j : Nat) (hji : j < a), p xs[j] = false) ∧ a + 1 = i) ↔
    ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), p (x :: xs)[j] = false

Proof state:
case cons.isFalse.mp.intro.intro.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
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 + 1 < a + 1
⊢ p (x :: xs)[j + 1] = false

Tactic:
apply h₂

Result:
case cons.isFalse.mp.intro.intro.intro.intro.succ.hji
α : 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 + 1 < a + 1
⊢ j < a

Proof state:
case cons.isFalse.mp
α : 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
⊢ (∃ a, (∃ h, p xs[a] = true ∧ ∀ (j : Nat) (hji : j < a), p xs[j] = false) ∧ a + 1 = i) →
    ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), p (x :: xs)[j] = false

Tactic:
rintro ⟨a, ⟨⟨h, h₁, h₂⟩, rfl⟩⟩

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
⊢ ∃ h, p (x :: xs)[a + 1] = true ∧ ∀ (j : Nat) (hji : j < a + 1), p (x :: xs)[j] = false

Proof state:
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

Tactic:
simp only [Option.some.injEq, Bool.not_eq_true, length_cons]

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
⊢ 0 = i ↔ ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), p (x :: xs)[j] = false

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
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
⊢ p xs[i] = true

Tactic:
simpa

Result:
no goals

Proof state:
case cons.isFalse.mp.intro.intro.intro.intro.succ.hji
α : 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 + 1 < a + 1
⊢ j < a

Tactic:
simp_all [Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
case cons.isFalse.mpr
α : 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, p (x :: xs)[i] = true ∧ ∀ (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:
rintro ⟨h, h₁, h₂⟩

Result:
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

Proof state:
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
⊢ (∃ a, (∃ h, p xs[a] = true ∧ ∀ (j : Nat) (hji : j < a), p xs[j] = false) ∧ a + 1 = i) ↔
    ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), p (x :: xs)[j] = false

Tactic:
constructor

Result:
case cons.isFalse.mp
α : 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
⊢ (∃ a, (∃ h, p xs[a] = true ∧ ∀ (j : Nat) (hji : j < a), p xs[j] = false) ∧ a + 1 = i) →
    ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), p (x :: xs)[j] = false

case cons.isFalse.mpr
α : 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, p (x :: xs)[i] = true ∧ ∀ (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

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
⊢ findIdx? p (x :: xs) = some i ↔ ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), ¬p (x :: xs)[j] = true

Tactic:
simp only [findIdx?_cons, Nat.zero_add]

Result:
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

Proof state:
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
⊢ 0 = i ↔ ∃ h, p (x :: xs)[i] = true ∧ ∀ (j : Nat) (hji : j < i), p (x :: xs)[j] = false

Tactic:
cases i with
| zero => simp_all
| succ i =>
  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]
  intros
  refine ⟨0, zero_lt_succ i, ‹_›⟩

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
j : Nat
hj : j < a + 1
⊢ p (x :: xs)[j] = false

Tactic:
cases j with
| zero => simp_all
| succ j =>
  apply h₂
  simp_all [Nat.succ_lt_succ_iff]

Result:
no goals