α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
⊢ (rfindOpt f).Dom
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
⊢ (rfindOpt f).Dom
have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
⊢ (rfindOpt f).Dom
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
⊢ (rfindOpt f).Dom
have s := Nat.find_spec h'
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
⊢ (rfindOpt f).Dom
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
⊢ (rfindOpt f).Dom
have fd : (rfind fun n => (f n).isSome).Dom :=
  ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
⊢ ((fun b => (fun n => ↑(f n)) (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) b)) fd).Dom
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
⊢ (rfindOpt f).Dom
refine' ⟨fd, _⟩
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this : true ∈ ↑(Option.some (Option.isSome (f (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) fd))))
⊢ ((fun b => (fun n => ↑(f n)) (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) b)) fd).Dom
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
⊢ ((fun b => (fun n => ↑(f n)) (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) b)) fd).Dom
have := rfind_spec (get_mem fd)
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
⊢ Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom))) =
    true
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this : true ∈ ↑(Option.some (Option.isSome (f (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) fd))))
⊢ ((fun b => (fun n => ↑(f n)) (Part.get (rfind fun n => ↑(Option.some (Option.isSome (f n)))) b)) fd).Dom
simp at this⊢
case intro
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
a : α
e :
  f
      (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
        (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)) =
    Option.some a
⊢ Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom))) =
    true
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
⊢ Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom))) =
    true
cases' Option.isSome_iff_exists.1 this.symm with a e
case intro
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
a : α
e :
  f
      (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
        (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)) =
    Option.some a
⊢ Option.isSome (Option.some a) = true
case intro
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
a : α
e :
  f
      (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
        (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)) =
    Option.some a
⊢ Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom))) =
    true
rw [e]
no goals
case intro
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
fd : (rfind fun n => ↑(Option.some (Option.isSome (f n)))).Dom
this :
  true =
    Option.isSome
      (f
        (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
          (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)))
a : α
e :
  f
      (Part.get (rfind fun n => Part.some (Option.isSome (f n)))
        (_ : (rfind fun n => Part.some (Option.isSome (f n))).Dom)) =
    Option.some a
⊢ Option.isSome (Option.some a) = true
trivial
no goals
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, Option.isSome (f n) = true
s : Option.isSome (f (Nat.find h')) = true
⊢ true ∈ (fun n => ↑(Option.some (Option.isSome (f n)))) (Nat.find h')
simpa using s.symm