-- Mathlib/Computability/Partrec.lean
theorem rfindOpt_dom {α} {f : ℕ → Option α} : (rfindOpt f).Dom ↔ ∃ n a, a ∈ f n :=
  ⟨fun h => (rfindOpt_spec ⟨h, rfl⟩).imp fun _ h => ⟨_, h⟩, fun h => by
    have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2
    have s := Nat.find_spec h'
    have fd : (rfind fun n => (f n).isSome).Dom :=
      ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩
    refine ⟨fd, ?_⟩
    have := rfind_spec (get_mem fd)
    simpa using this⟩

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
⊢ true ∈ (fun n => ↑(Option.some (f n).isSome)) (Nat.find h')

Tactic:
simpa using s.symm

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
⊢ (rfindOpt f).Dom

Tactic:
have fd : (rfind fun n => (f n).isSome).Dom :=
  ⟨Nat.find h', by simpa using s.symm, fun _ _ => trivial⟩

Result:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom
⊢ (rfindOpt f).Dom

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
⊢ (rfindOpt f).Dom

Tactic:
have s := Nat.find_spec h'

Result:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
⊢ (rfindOpt f).Dom

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom
this : true ∈ ↑(Option.some (f ((rfind fun n => ↑(Option.some (f n).isSome)).get fd)).isSome)
⊢ ((fun b => (fun n => ↑(f n)) ((rfind fun n => ↑(Option.some (f n).isSome)).get b)) fd).Dom

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom
⊢ (rfindOpt f).Dom

Tactic:
refine ⟨fd, ?_⟩

Result:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom
⊢ ((fun b => (fun n => ↑(f n)) ((rfind fun n => ↑(Option.some (f n).isSome)).get b)) fd).Dom

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
⊢ (rfindOpt f).Dom

Tactic:
have h' : ∃ n, (f n).isSome := h.imp fun n => Option.isSome_iff_exists.2

Result:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
⊢ (rfindOpt f).Dom

Proof state:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom
⊢ ((fun b => (fun n => ↑(f n)) ((rfind fun n => ↑(Option.some (f n).isSome)).get b)) fd).Dom

Tactic:
have := rfind_spec (get_mem fd)

Result:
α : Type u_1
f : ℕ → Option α
h : ∃ n a, a ∈ f n
h' : ∃ n, (f n).isSome = true
s : (f (Nat.find h')).isSome = true
fd : (rfind fun n => ↑(Option.some (f n).isSome)).Dom
this : true ∈ ↑(Option.some (f ((rfind fun n => ↑(Option.some (f n).isSome)).get fd)).isSome)
⊢ ((fun b => (fun n => ↑(f n)) ((rfind fun n => ↑(Option.some (f n).isSome)).get b)) fd).Dom