-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem find_min :
    ∀ {n : ℕ} {p : Fin n → Prop} [DecidablePred p] {i : Fin n} (_ : i ∈ Fin.find p) {j : Fin n}
      (_ : j < i), ¬p j
  | 0, _, _, _, hi, _, _, _ => Option.noConfusion hi
  | n + 1, p, _, i, hi, ⟨j, hjn⟩, hj, hpj => by
    rw [find] at hi
    rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | k
    · simp only [h] at hi
      split_ifs at hi with hl
      · cases hi
        rw [find_eq_none_iff] at h
        exact h ⟨j, hj⟩ hpj
      · exact Option.not_mem_none _ hi
    · rw [h] at hi
      dsimp at hi
      obtain rfl := Option.some_inj.1 hi
      exact find_min h (show (⟨j, lt_trans hj k.2⟩ : Fin n) < k from hj) hpj

Proof state:
case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ False

Tactic:
exact Option.not_mem_none _ hi

Result:
no goals

Proof state:
case pos
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ False

Tactic:
cases hi

Result:
case pos.refl
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hj : ⟨j, hjn⟩ < last n
⊢ False

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
k : Fin n
h : (find fun i => p (i.castLT ⋯)) = some k
⊢ False

Tactic:
rw [h] at hi

Result:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
k : Fin n
hi : i ∈ Option.casesOn (some k) (if x : p (last n) then some (last n) else none) fun i => some (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some k
⊢ False

Proof state:
case none
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
⊢ False

Tactic:
simp only [h] at hi

Result:
case none
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hi : i ∈ if x : p (last n) then some (last n) else none
⊢ False

Proof state:
case pos.refl
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p ⟨j, hjn⟩
h : ∀ (i : Fin n), ¬p (i.castLT ⋯)
hl : p (last n)
hj : ⟨j, hjn⟩ < last n
⊢ False

Tactic:
exact h ⟨j, hj⟩ hpj

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : i ∈ find p
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
⊢ False

Tactic:
rw [find] at hi

Result:
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
⊢ False

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
k : Fin n
hi : i ∈ Option.casesOn (some k) (if x : p (last n) then some (last n) else none) fun i => some (i.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some k
⊢ False

Tactic:
dsimp at hi

Result:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
k : Fin n
hi : i ∈ some (k.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some k
⊢ False

Proof state:
case none
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hi : i ∈ if x : p (last n) then some (last n) else none
⊢ False

Tactic:
split_ifs at hi with hl

Result:
case pos
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hi : i ∈ some (last n)
⊢ False

case neg
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : ¬p (last n)
hi : i ∈ none
⊢ False

Proof state:
case pos.refl
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
hl : p (last n)
hj : ⟨j, hjn⟩ < last n
⊢ False

Tactic:
rw [find_eq_none_iff] at h

Result:
case pos.refl
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p ⟨j, hjn⟩
h : ∀ (i : Fin n), ¬p (i.castLT ⋯)
hl : p (last n)
hj : ⟨j, hjn⟩ < last n
⊢ False

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
k : Fin n
hi : i ∈ some (k.castLT ⋯)
h : (find fun i => p (i.castLT ⋯)) = some k
⊢ False

Tactic:
obtain rfl := Option.some_inj.1 hi

Result:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p ⟨j, hjn⟩
k : Fin n
h : (find fun i => p (i.castLT ⋯)) = some k
hj : ⟨j, hjn⟩ < k.castLT ⋯
hi : k.castLT ⋯ ∈ some (k.castLT ⋯)
⊢ False

Proof state:
case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
j : ℕ
hjn : j < n + 1
hpj : p ⟨j, hjn⟩
k : Fin n
h : (find fun i => p (i.castLT ⋯)) = some k
hj : ⟨j, hjn⟩ < k.castLT ⋯
hi : k.castLT ⋯ ∈ some (k.castLT ⋯)
⊢ False

Tactic:
exact find_min h (show (⟨j, lt_trans hj k.2⟩ : Fin n) < k from hj) hpj

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
⊢ False

Tactic:
rcases h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with - | k

Result:
case none
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
h : (find fun i => p (i.castLT ⋯)) = none
⊢ False

case some
n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi :
  i ∈
    Option.casesOn (find fun i => p (i.castLT ⋯)) (if x : p (last n) then some (last n) else none) fun i =>
      some (i.castLT ⋯)
j : ℕ
hjn : j < n + 1
hj : ⟨j, hjn⟩ < i
hpj : p ⟨j, hjn⟩
k : Fin n
h : (find fun i => p (i.castLT ⋯)) = some k
⊢ False