Chain option some

theorem chain_option_some [OFE V] {c : Chain (Option V)} (H : c n = some v) :    ∃ c' : Chain V, c = Chain.map ⟨some, OFE.Option.some.ne⟩ c' := by  have HVc (k) : ∃ v', c k = some v' := by    rcases h : c.chain k with (_|v')    · simp [chain_none_const h] at H    · exists v'  let c' : Chain V :=    ⟨fun n => Classical.choose <| HVc n,     by       intro n i Hni       have HR := c.cauchy Hni       rw [Classical.choose_spec (HVc n), Classical.choose_spec (HVc i)] at HR       exact HR ⟩  exists c'  rcases hcc : c with ⟨cc, Hcc⟩  simp only [Chain.map, Chain.mk.injEq]  refine funext (fun i => ?_)  simp only [c']  have Hchoose := Classical.choose_spec (HVc i)  rw [← Hchoose]  simp [hcc]