Reduction all Verdicts eq map all Outputs fst

lemma Reduction.allVerdicts_eq_map_allOutputs_fst {L : ℕ} {β : Type}    (extract : ((FullTranscript pSpec × StmtOut × WitOut) × StmtOut) → β)    (stmts : Fin L → StmtIn) (wits : Fin L → WitIn)    (reduction : Reduction oSpec StmtIn WitIn StmtOut WitOut pSpec) :    reduction.allVerdicts stmts wits =      (Option.map (fun resultOf => fun i => (resultOf i).1)) <$>        reduction.allOutputs (fun result => (result.2, extract result)) stmts wits := by  unfold Reduction.allVerdicts Reduction.allOutputs Reduction.allRuns  simp only [map_eq_bind_pure_comp, bind_assoc, pure_bind, Function.comp_apply]  rw [Vector.mapM_bind_map_eq    (v := Vector.ofFn (id : Fin L → Fin L))    (f₁ := fun i => (reduction.verdict (stmts i) (wits i)).run)    (f₂ := fun i => (reduction.run (stmts i) (wits i)).run)    (g := Option.map (fun result : (FullTranscript pSpec × StmtOut × WitOut) × StmtOut =>      result.2))    (post₁ := fun results =>      pure ((results.mapM id).map fun v => fun i => v[i]))    (post₂ := fun results =>      pure (Option.map (fun resultOf => fun i => (resultOf i).1)        (Option.map (fun resultOf => fun i => ((resultOf i).2, extract (resultOf i)))          (Option.map (fun v => fun i => v[i]) (results.mapM id)))))]  · intro i    exact Reduction.verdict_run_eq_map_run reduction (stmts i) (wits i)  · intro results    congr 1    rw [Vector.mapM_id_option_map_comm]    cases h : results.mapM id with    | none => simp    | some v =>        simp only [Option.map_some, Option.some.injEq]        funext i        simp