Verifier id knowledge Soundness

@[simp]theorem Verifier.id_knowledgeSoundness {rel : Set (StmtIn × WitIn)} :    (Verifier.id : Verifier oSpec _ _ _).knowledgeSoundness init impl rel rel 0 := by  -- `Extractor.Straightline.id` returns the (adversarial) output witness. On the support of the  -- game, the identity verifier outputs the input statement, so the bad event requires both  -- `(stmtIn, witOut) ∉ rel` (extracted witness invalid) and `(stmtIn, witOut) ∈ rel`  -- (output pair valid): a contradiction.  refine ⟨Extractor.Straightline.id, fun stmtIn witIn prover => ?_⟩  simp only [ENNReal.coe_zero, le_zero_iff]  refine probEvent_eq_zero fun x hx => ?_  rw [OptionT.mem_support_iff, OptionT.run_mk] at hx  simp only [support_bind, Set.mem_iUnion] at hx  obtain ⟨s, _, hx⟩ := hx  simp only [Reduction.runWithLog, Verifier.run, Verifier.id, Extractor.Straightline.id,    OptionT.run_bind, OptionT.run_pure, Option.getM, Option.elimM,    simulateQ_bind, StateT.run'_bind', support_bind, Set.mem_iUnion] at hx  obtain ⟨⟨o, s'⟩, hi, hx2⟩ := hx  cases o with  | none =>    simp only [Option.elim, simulateQ_pure, StateT.run'_pure', support_pure,      Set.mem_singleton_iff] at hx2    exact (Option.some_ne_none x hx2).elim  | some x' =>    -- From `hx2`: `x = (stmtIn, some witOut, x'.1.2, witOut)`    simp only [Option.elim, simulateQ_pure, OptionT.run_pure, liftM_pure, pure_bind,      StateT.run'_pure', support_pure, Set.mem_singleton_iff] at hx2    -- From `hi`: the verifier is the identity, so `x'.1.2 = stmtIn`    rw [show (pure stmtIn : OptionT (OracleComp oSpec) StmtIn) =      (pure (some stmtIn) : OracleComp oSpec (Option StmtIn)) from rfl] at hi    simp only [Option.elim, simulateQ_pure, OptionT.run_pure, WriterT.run_pure, liftM_pure,      pure_bind, support_bind, Set.mem_iUnion, StateT.run_bind] at hi    obtain ⟨⟨o2, s2⟩, _, hi2⟩ := hi    cases o2 with    | none =>      simp only [simulateQ_pure, StateT.run_pure, support_pure,        Set.mem_singleton_iff, Prod.mk.injEq] at hi2      exact (Option.some_ne_none x' hi2.1).elim    | some pr =>      simp only [simulateQ_pure, StateT.run_pure, support_pure,        Set.mem_singleton_iff, Prod.mk.injEq, Option.some.injEq] at hi2      obtain ⟨rfl, -⟩ := hi2      simp only [Option.some.injEq] at hx2      subst hx2      rintro ⟨h1, h2⟩      exact h1 _ rfl h2