-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem not_of_lt_findIdx {p : α → Bool} {xs : List α} {i : Nat} (h : i < xs.findIdx p) :
    p (xs[i]'(Nat.le_trans h (findIdx_le_length p))) = false

Proof state:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
e : i > 0
ipm : i.pred.succ = i
⊢ p (x :: xs)[i] = false

Tactic:
simp +singlePass only [← ipm, getElem_cons_succ]

Result:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
e : i > 0
ipm : i.pred.succ = i
⊢ p xs[i.pred] = false

Proof state:
case a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < 0
ho : i < findIdx p (x :: xs)
y : p x = true
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h : i < findIdx p (x :: xs)
⊢ p (x :: xs)[i] = false

Tactic:
have ho := h

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h ho : i < findIdx p (x :: xs)
⊢ p (x :: xs)[i] = false

Proof state:
case a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
⊢ ¬p x = true

Tactic:
intro y

Result:
case a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
y : p x = true
⊢ False

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
⊢ p x = false

Tactic:
apply eq_false_of_ne_true

Result:
case a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
⊢ ¬p x = true

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
⊢ p (x :: xs)[i] = false

Tactic:
cases i.eq_zero_or_pos with
| inl e => simpa [e, Fin.zero_eta, get_cons_zero]
| inr e =>
  have ipm := Nat.succ_pred_eq_of_pos e
  simp +singlePass only [← ipm, getElem_cons_succ]
  rw [← ipm, Nat.succ_lt_succ_iff] at h
  simpa using ih h

Result:
no goals

Proof state:
case cons.inl
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
e : i = 0
⊢ p (x :: xs)[i] = false

Tactic:
simpa [e, Fin.zero_eta, get_cons_zero]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
i : Nat
h : i < findIdx p xs
⊢ p xs[i] = false

Tactic:
revert i

Result:
α : Type u_1
p : α → Bool
xs : List α
⊢ ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false

Proof state:
case a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
y : p x = true
⊢ False

Tactic:
rw [y, cond_true] at h

Result:
case a
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < 0
ho : i < findIdx p (x :: xs)
y : p x = true
⊢ False

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
⊢ p (x :: xs)[i] = false

Tactic:
have npx : p x = false := by
  apply eq_false_of_ne_true
  intro y
  rw [y, cond_true] at h
  simp at h

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
npx : p x = false
⊢ p (x :: xs)[i] = false

Proof state:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
e : i > 0
⊢ p (x :: xs)[i] = false

Tactic:
have ipm := Nat.succ_pred_eq_of_pos e

Result:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
e : i > 0
ipm : i.pred.succ = i
⊢ p (x :: xs)[i] = false

Proof state:
case nil
α : Type u_1
p : α → Bool
i : Nat
h : i < findIdx p []
⊢ p [][i] = false

Tactic:
rw [findIdx_nil] at h

Result:
case nil
α : Type u_1
p : α → Bool
i : Nat
h✝ : i < findIdx p []
h : i < 0
⊢ p [][i] = false

Proof state:
case cons.inr
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i.pred < findIdx p xs
e : i > 0
ipm : i.pred.succ = i
⊢ p xs[i.pred] = false

Tactic:
simpa using ih h

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
⊢ ∀ {i : Nat} (h : i < findIdx p (x :: xs)), p (x :: xs)[i] = false

Tactic:
intro i h

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h : i < findIdx p (x :: xs)
⊢ p (x :: xs)[i] = false

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h ho : i < findIdx p (x :: xs)
⊢ p (x :: xs)[i] = false

Tactic:
rw [findIdx_cons] at h

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
⊢ p (x :: xs)[i] = false

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ ∀ {i : Nat} (h : i < findIdx p []), p [][i] = false

Tactic:
intro i h

Result:
case nil
α : Type u_1
p : α → Bool
i : Nat
h : i < findIdx p []
⊢ p [][i] = false

Proof state:
case nil
α : Type u_1
p : α → Bool
i : Nat
h✝ : i < findIdx p []
h : i < 0
⊢ p [][i] = false

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ : i < findIdx p (x :: xs)
h : i < bif p x then 0 else findIdx p xs + 1
ho : i < findIdx p (x :: xs)
npx : p x = false
⊢ p (x :: xs)[i] = false

Tactic:
simp [npx, cond_false] at h

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : ∀ {i : Nat} (h : i < findIdx p xs), p xs[i] = false
i : Nat
h✝ ho : i < findIdx p (x :: xs)
npx : p x = false
h : i < findIdx p xs + 1
⊢ p (x :: xs)[i] = false