Run Trace target eq of mem context Fork

lemma runTrace_target_eq_of_mem_contextFork    [DecidableEq M] [DecidableEq Commit] [DecidableEq Chal] [SampleableType Chal] [Inhabited Chal]    (nmaAdv : SignatureAlg.managedRoNmaAdv      (FiatShamir (m := OracleComp (unifSpec + (M × Commit →ₒ Chal))) σ hr M))    (qH : ℕ) (pk : Stmt)    (x₁ x₂ : Trace (M := M) (Commit := Commit) (Resp := Resp) (Chal := Chal))    (s : Fin (qH + 1))    (hsup : some (x₁, x₂) ∈ support (contextFork (runTrace σ hr M nmaAdv pk)      (fun j : ℕ ⊕ Unit => match j with | .inl _ => 0 | .inr () => qH) (Sum.inr ())      (forkPoint (M := M) (Commit := Commit) (Resp := Resp) (Chal := Chal) qH)))    (h₁ : forkPoint (M := M) (Commit := Commit) (Resp := Resp) (Chal := Chal)      qH x₁ = some s)    (h₂ : forkPoint (M := M) (Commit := Commit) (Resp := Resp) (Chal := Chal)      qH x₂ = some s) :    x₁.target = x₂.target := by  letI : Fintype Chal := Fintype.ofFinite Chal  letI : IsUniformSpec ((Unit →ₒ Chal) : OracleSpec _) :=    IsUniformSpec.ofFintypeInhabited _  let qb : ℕ ⊕ Unit → ℕ := fun j => match j with | .inl _ => 0 | .inr () => qH  let cf := forkPoint (M := M) (Commit := Commit) (Resp := Resp) (Chal := Chal) qH  let main := runTrace σ hr M nmaAdv pk  obtain ⟨path, s', located, second, hpath, hcf₁, _hsecond,      _hne, _hcf₂, hx₁, hx₂⟩ :=    contextFork_success main qb (Sum.inr ()) cf hsup  have hs' : s' = s := by    apply Option.some.inj    calc      some s' = cf (PFunctor.FreeM.output main path) := hcf₁.symm      _ = cf x₁ := by rw [hx₁]      _ = some s := h₁  subst s'  let commonLog : QueryLog (wrappedSpec Chal) := located.occurrence.before  have hfirst := replayPathResult_mem_support_replayFirstRun main path hpath  have hsecond := replayPathResult_mem_support_replayFirstRun main second.path    (mem_support_replayFirstPath main second.path)  have hxlog₁ : (x₁, (replayPathResult main path).2) ∈      support (replayFirstRun main) := by    simpa [replayPathResult, pathLogResult, hx₁] using hfirst  have hxlog₂ : (x₂, (replayPathResult main second.path).2) ∈      support (replayFirstRun main) := by    simpa [replayPathResult, pathLogResult, hx₂] using hsecond  have hlog₁ : (replayPathResult main path).2 =      commonLog ++        (⟨Sum.inr (), located.completion.answer⟩ ::          (replayPathResult (located.occurrence.resume            located.completion.answer) located.completion.suffix).2) := by    have htrace := congrArg      (fun p : PFunctor.FreeM.Path main =>        (show QueryLog (wrappedSpec Chal) from          PFunctor.FreeM.Path.trace main p)) located.path_eq    calc      (replayPathResult main path).2          = (replayPathResult main located.completion.path).2 := htrace.symm      _ = _ := by        change PFunctor.FreeM.Path.trace main located.completion.path =          List.append            (show PFunctor.TraceList (wrappedSpec Chal).toPFunctor from              commonLog)            (⟨Sum.inr (), located.completion.answer⟩ ::              PFunctor.FreeM.Path.trace                (located.occurrence.resume located.completion.answer)                located.completion.suffix)        unfold commonLog        exact PFunctor.FreeM.Cursor.Occurrence.trace_plug          located.occurrence located.completion.answer            located.completion.suffix  have hlog₂ : (replayPathResult main second.path).2 =      commonLog ++        (⟨Sum.inr (), second.answer⟩ ::          (replayPathResult (located.occurrence.resume second.answer)            second.suffix).2) := by    change PFunctor.FreeM.Path.trace main second.path =      List.append        (show PFunctor.TraceList (wrappedSpec Chal).toPFunctor from          commonLog)        (⟨Sum.inr (), second.answer⟩ ::          PFunctor.FreeM.Path.trace            (located.occurrence.resume second.answer) second.suffix)    unfold commonLog    exact PFunctor.FreeM.Cursor.Occurrence.trace_plug      located.occurrence second.answer second.suffix  have htakeEq := runTrace_queryLog_take_eq σ hr M (Resp := Resp) nmaAdv pk    (x₁ := x₁) (x₂ := x₂)    (outerLog₁ := (replayPathResult main path).2)    (outerLog₂ := (replayPathResult main second.path).2)    hxlog₁ hxlog₂    (p := commonLog)    (v₁ := located.completion.answer) (v₂ := second.answer)    (rest₁ := (replayPathResult (located.occurrence.resume      located.completion.answer) located.completion.suffix).2)    (rest₂ := (replayPathResult (located.occurrence.resume second.answer)      second.suffix).2) hlog₁ hlog₂  have hprefixCount : commonLog.countQ      (fun x => x = Sum.inr ()) = (↑s : ℕ) := by    calc      commonLog.countQ (fun x => x = Sum.inr ()) =          PFunctor.TraceList.occurrences (P := (wrappedSpec Chal).toPFunctor)            (Sum.inr ())            (show PFunctor.TraceList (wrappedSpec Chal).toPFunctor from              commonLog) := QueryLog.countQ_eq_occurrences commonLog (Sum.inr ())      _ = (↑s : ℕ) := by        simp [commonLog]  rw [hprefixCount] at htakeEq  have htgt₁ : x₁.queryLog[(↑s : ℕ)]? = some x₁.target :=    forkPoint_getElem?_eq_some_target (M := M) (Commit := Commit) (Resp := Resp)      (Chal := Chal) h₁  have htgt₂ : x₂.queryLog[(↑s : ℕ)]? = some x₂.target :=    forkPoint_getElem?_eq_some_target (M := M) (Commit := Commit) (Resp := Resp)      (Chal := Chal) h₂  have hgetElemTake (l : List (M × Commit)) :      (l.take ((↑s : ℕ) + 1))[(↑s : ℕ)]? = l[(↑s : ℕ)]? :=    List.getElem?_take_of_lt (Nat.lt_succ_self _)  apply Option.some.inj  rw [← htgt₁, ← htgt₂, ← hgetElemTake x₁.queryLog,    ← hgetElemTake x₂.queryLog, htakeEq]