m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : ∃ a, find p = some a
⊢ ∃ i, p i
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : Option.isSome (find p) = true
⊢ ∃ i, p i
rw [Option.isSome_iff_exists] at h
case intro
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : find p = some i
⊢ ∃ i, p i
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
h : ∃ a, find p = some a
⊢ ∃ i, p i
cases' h with i hi
no goals
case intro
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝ : DecidablePred p
i : Fin (n + 1)
hi : find p = some i
⊢ ∃ i, p i
exact ⟨i, find_spec _ hi⟩
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
⊢ Option.isSome
      (Option.rec (if p (last (n + 0)) then some (last (n + 0)) else none)
        (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0))))
        (find fun i => p (castLT i (_ : ↑i < Nat.succ (n + 0))))) =
    true
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
⊢ Option.isSome (find p) = true
dsimp [find]
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ Option.isSome
      (Option.rec (if p (last (n + 0)) then some (last (n + 0)) else none)
        (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) =
    true

case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
j : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ Option.isSome
      (Option.rec (if p (last (n + 0)) then some (last (n + 0)) else none)
        (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) (some j)) =
    true
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
⊢ Option.isSome
      (Option.rec (if p (last (n + 0)) then some (last (n + 0)) else none)
        (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0))))
        (find fun i => p (castLT i (_ : ↑i < Nat.succ (n + 0))))) =
    true
cases' h : find fun i : Fin n ↦ p (i.castLT (Nat.lt_succ_of_lt i.2)) with j
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last (n + 0))
⊢ Option.isSome (Option.rec (some (last (n + 0))) (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) =
    true

case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) = true
case none
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
⊢ Option.isSome
      (Option.rec (if p (last (n + 0)) then some (last (n + 0)) else none)
        (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) =
    true
split_ifs with hl
no goals
case none.inl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : p (last (n + 0))
⊢ Option.isSome (Option.rec (some (last (n + 0))) (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) =
    true
exact Option.isSome_some
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
this : Option.isSome (find fun x => p (castLT x (_ : ↑x < Nat.succ n))) = true
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) = true
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) = true
have := (@isSome_find_iff n (fun x ↦ p (x.castLT (Nat.lt_succ_of_lt x.2))) _).2
    ⟨⟨i, lt_of_le_of_ne (Nat.le_of_lt_succ hin) fun h ↦ by cases h; exact hl hi⟩, hi⟩
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
this : Option.isSome none = true
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) = true
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
this : Option.isSome (find fun x => p (castLT x (_ : ↑x < Nat.succ n))) = true
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) = true
rw [h] at this
no goals
case none.inr
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
this : Option.isSome none = true
⊢ Option.isSome (Option.rec none (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) none) = true
exact this
case refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
hin : n < n + 1
hi : p { val := n, isLt := hin }
⊢ False
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
h✝ : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
h : i = n
⊢ False
cases h
no goals
case refl
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = none
hl : ¬p (last (n + 0))
hin : n < n + 1
hi : p { val := n, isLt := hin }
⊢ False
exact hl hi
no goals
case some
m n✝ n : ℕ
p : Fin (n + 1) → Prop
x✝¹ : DecidablePred p
x✝ : ∃ i, p i
i : ℕ
hin : i < n + 1
hi : p { val := i, isLt := hin }
j : Fin n
h : (find fun i => p (castLT i (_ : ↑i < Nat.succ n))) = some j
⊢ Option.isSome
      (Option.rec (if p (last (n + 0)) then some (last (n + 0)) else none)
        (fun val => some (castLT val (_ : ↑val < Nat.succ (n + 0)))) (some j)) =
    true
simp