Advantage le module SIS

theorem advantage_le_moduleSIS (base : ZMod q)    (hq5 : q % 8 = 5) (βSq γ κ : Nat) (hκ : κ ^ 2 < q)    (adv :      Adversary 𝓜(q, α) innerRows messageRows messageDigits outerRows blocks innerDigits) :    advantage 𝓜(q, α) base βSq γ κ adv ≤      ModuleSIS.advantage 𝓜(q, α) innerRows (messageRows * messageDigits)          (innerShort 𝓜(q, α) κ βSq)          (innerAdvToModuleSIS 𝓜(q, α) (innerShort 𝓜(q, α) κ βSq) adv) +        ModuleSIS.advantage 𝓜(q, α) outerRows (blocks * (innerRows * innerDigits))          (outerShort 𝓜(q, α) γ)          (outerAdvToModuleSIS 𝓜(q, α) (outerShort 𝓜(q, α) γ) adv) := by  unfold advantage experiment ModuleSIS.advantage SIS.advantage SIS.experiment    ModuleSIS.problem innerAdvToModuleSIS outerAdvToModuleSIS  simp only [monad_norm]  rw [← probOutput_bind_bind_swap    ($ᵗ (Simple.PublicParams 𝓜(q, α) innerRows (messageRows * messageDigits)))    ($ᵗ (Simple.PublicParams 𝓜(q, α) outerRows (blocks * (innerRows * innerDigits)))) _ true]  refine probOutput_bind_congr_le_add    (mx := $ᵗ (Simple.PublicParams 𝓜(q, α) innerRows (messageRows * messageDigits)))    (y := true) (z₁ := true) (z₂ := true) (fun A _ => ?_)  refine probOutput_bind_congr_le_add    (mx := $ᵗ (Simple.PublicParams 𝓜(q, α) outerRows (blocks * (innerRows * innerDigits))))    (y := true) (z₁ := true) (z₂ := true) (fun B _ => ?_)  refine probOutput_bind_congr_le_add    (mx := adv { innerMatrix := A, outerMatrix := B })    (y := true) (z₁ := true) (z₂ := true) (fun x _ => ?_)  obtain ⟨u, opening₁, opening₂⟩ := x  have hs := sample_advantage_le_moduleSIS α base hq5 βSq γ κ hκ A B u    opening₁ opening₂  cases hsol : outputToModuleSIS 𝓜(q, α) opening₁ opening₂ with  | inl z => rw [hsol] at hs; simpa using hs  | inr z => rw [hsol] at hs; simpa using hs