Sample advantage le module SIS

theorem sample_advantage_le_moduleSIS (base : ZMod q)    (hq5 : q % 8 = 5) (βSq γ κ : Nat) (hκ : κ ^ 2 < q)    (A : Simple.PublicParams 𝓜(q, α) innerRows (messageRows * messageDigits))    (B : Simple.PublicParams 𝓜(q, α) outerRows (blocks * (innerRows * innerDigits)))    (u : Commitment 𝓜(q, α) outerRows)    (opening₁ opening₂ :      Opening 𝓜(q, α) innerRows messageRows messageDigits blocks innerDigits) :    Pr[= true | ((pure (openingsDiffer 𝓜(q, α) opening₁ opening₂ &&        verify_weak 𝓜(q, α) base βSq γ κ          { innerMatrix := A, outerMatrix := B } u opening₁ &&        verify_weak 𝓜(q, α) base βSq γ κ          { innerMatrix := A, outerMatrix := B } u opening₂)) :        ProbComp Bool)] ≤      Pr[= true | ((pure (ModuleSIS.relation 𝓜(q, α) (innerShort 𝓜(q, α) κ βSq)          A (match outputToModuleSIS 𝓜(q, α) opening₁ opening₂ with            | Sum.inl z => z            | Sum.inr _ => dummySolution 𝓜(q, α) (messageRows * messageDigits)))) :          ProbComp Bool)] +      Pr[= true | ((pure (ModuleSIS.relation 𝓜(q, α) (outerShort 𝓜(q, α) γ)          B (match outputToModuleSIS 𝓜(q, α) opening₁ opening₂ with            | Sum.inl _ => dummySolution 𝓜(q, α) (blocks * (innerRows * innerDigits))            | Sum.inr z => z))) :          ProbComp Bool)] := by  let pp : PublicParams 𝓜(q, α)      innerRows messageRows messageDigits outerRows blocks innerDigits :=    { innerMatrix := A, outerMatrix := B }  refine probOutput_pure_bool_le_or _ _ _ (fun hwin => ?_)  have hvalid := outputToModuleSIS_valid α base hq5 βSq γ κ hκ pp u    opening₁ opening₂ hwin  cases hsol : outputToModuleSIS 𝓜(q, α) opening₁ opening₂ with  | inl z => exact Or.inl (by rw [hsol] at hvalid; simpa [hsol, pp] using hvalid)  | inr z => exact Or.inr (by rw [hsol] at hvalid; simpa [hsol, pp] using hvalid)